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 560  a12lem1 1415  mo 1432  peano5 3241  tfrlem1 4212  dfuzi 6373  uzindOLD 6379  fsump1s 7216  fsumcmp 7243  fsumcmpndx2 7245  climconsti 7297  caucvglem5 7364  caucvglem6 7365  fsum0diaglem2 7462  clsval2 7895  cnpco 7979  cncnplem4 7987  metreslem 8032  metcnpi3 8103  metcnpi4 8104  metcni2 8106  metcnp4 8181  xpcn 8187  lmcau 8207  dmdmd 10508  mdsl0 10518  mdsl1i 10529  ghomf1olem 10681  compfipin0lem 11492  compfipin0 11493  totbndbnd 12000  heiborlem16 12026

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

Copyright terms: Public domain