HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem imim12d 29
Description: Deduction combining antecedents and consequents.
Hypotheses
Ref Expression
imim12d.1 |- (ph -> (ps -> ch))
imim12d.2 |- (ph -> (th -> ta))
Assertion
Ref Expression
imim12d |- (ph -> ((ch -> th) -> (ps -> ta)))
Proof of Theorem imim12d
StepHypRef Expression
1 imim12d.1 . . 3 |- (ph -> (ps -> ch))
21imim1d 28 . 2 |- (ph -> ((ch -> th) -> (ps -> th)))
3 imim12d.2 . . 3 |- (ph -> (th -> ta))
43imim2d 25 . 2 |- (ph -> ((ps -> th) -> (ps -> ta)))
52, 4syld 27 1 |- (ph -> ((ch -> th) -> (ps -> ta)))
Colors of variables: wff set class
Syntax hints:   -> wi 3
This theorem is referenced by:  pm3.48 555  a12lem1 1369  mo 1386  peano5 3143  tfrlem1 3896  dfuz 6150  uzindOLD 6156  fsump1s 6951  fsumcmp 6978  fsumcmpndx2 6980  climconst 7031  caucvglem5 7097  caucvglem6 7098  fsum0diaglem2 7192  clsval2 7627  cnpco 7708  cncnplem4 7716  metreslem 7762  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metcnp4 7904  xpcn 7910  lmcau 7930  dmdmdt 10137  mdsl0 10145  mdsl1 10156  ghomf1olem 10301
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain