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  843  jaddc  850  hbimd  1553  19.21ht  1561  nfimd  1565  19.23t  1656  spimth  1714  ssuni  3766  nnmordi  6420  omnimkv  7038  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  facdiv  10516  facwordi  10518  bezoutlemmain  11722  bezoutlemaz  11727  bezoutlembz  11728  algcvgblem  11766  prmfac1  11866  cncfco  12786  limccnpcntop  12852  limccoap  12855  bj-rspgt  13164