Theorem imim2d 54

Description: Deduction adding nested antecedents. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
imim2d.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
imim2d	|- ( ph -> ( ( th -> ps ) -> ( th -> ch ) ) )

Proof of Theorem imim2d

Step	Hyp	Ref	Expression
1		imim2d.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	a1d 22	. 2 |- ( ph -> ( th -> ( ps -> ch ) ) )
3	2	a2d 26	1 |- ( ph -> ( ( th -> ps ) -> ( th -> ch ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  imim2  55  embantd  56  imim12d  74  anc2r  328  pm5.31  348  con4biddc  857  jaddc  864  hbimd  1573  19.21ht  1581  nfimd  1585  19.23t  1677  spimth  1735  ssuni  3833  nnmordi  6519  omnimkv  7156  caucvgsrlemoffcau  7799  caucvgsrlemoffres  7801  facdiv  10720  facwordi  10722  bezoutlemmain  12001  bezoutlemaz  12006  bezoutlembz  12007  algcvgblem  12051  prmfac1  12154  infpnlem1  12359  cncfco  14163  limccnpcntop  14229  limccoap  14232  bj-rspgt  14623