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

Step	Hyp	Ref	Expression
1		imim12d.1	. . 3 |- (ph -> (ps -> ch))
2	1	imim1d 28	. 2 |- (ph -> ((ch -> th) -> (ps -> th)))
3		imim12d.2	. . 3 |- (ph -> (th -> ta))
4	3	imim2d 25	. 2 |- (ph -> ((ps -> th) -> (ps -> ta)))
5	2, 4	syld 27	1 |- (ph -> ((ch -> th) -> (ps -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm3.48 555  a12lem1 1353  mo 1370  peano5 3116  tfrlem1 3850  dfuz 6101  uzindOLD 6107  fsump1s 6902  fsumcmp 6929  fsumcmpndx2 6931  climconst 6982  caucvglem5 7048  caucvglem6 7049  fsum0diaglem2 7143  clsval2 7578  cnpco 7656  cncnplem4 7664  metreslem 7710  metcnpi3 7779  metcnpi4 7780  metcni2 7782  metcnp4 7852  xpcn 7858  lmcau 7878  ghomf1olem 8663  dmdmdt 10351  mdsl0 10359  mdsl1 10370

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain