Theorem imim12d 69

Description: Deduction combining antecedents and consequents. (The proof was shortened by O'Cat, 30-Oct-2011.)

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.2	. . 3 |- (ph -> (th -> ta))
2	1	imim2d 28	. 2 |- (ph -> ((ch -> th) -> (ch -> ta)))
3		imim12d.1	. 2 |- (ph -> (ps -> ch))
4	2, 3	syl5d 66	1 |- (ph -> ((ch -> th) -> (ps -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  jad 156  pm3.48 616  hbsb4t 1621  a12lem1 1767  mo 1787  peano5 3975  tfrlem1 5119  dfuzi 7414  uzindOLD 7420  fsump1s 8273  fsumcmp 8300  fsumcmpndx2 8302  climconsti 8354  caucvglem5 8421  caucvglem6 8422  fsum0diaglem2 8519  clsval2 8961  cnpco 9046  cncnplem4 9054  metreslem 9099  metcnpi3 9170  metcnpi4 9171  metcni2 9173  metcnp4 9248  xpcn 9254  lmcau 9274  dmdmd 11872  mdsl0 11882  mdsl1i 11893  ghomf1olem 13637  ax13dfeq 13865  fprodp1s 14682  compfipin0lem 15435  compfipin0 15436  totbndbnd 15944  heiborlem16 15970  ispridlc 16218  ax10ext 16364  smoge 16454

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

Copyright terms: Public domain