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  326  pm5.31  346  con4biddc  852  jaddc  859  hbimd  1566  19.21ht  1574  nfimd  1578  19.23t  1670  spimth  1728  ssuni  3818  nnmordi  6495  omnimkv  7132  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  facdiv  10672  facwordi  10674  bezoutlemmain  11953  bezoutlemaz  11958  bezoutlembz  11959  algcvgblem  12003  prmfac1  12106  infpnlem1  12311  cncfco  13372  limccnpcntop  13438  limccoap  13441  bj-rspgt  13821