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  858  jaddc  865  hbimd  1587  19.21ht  1595  nfimd  1599  19.23t  1691  spimth  1749  ssuni  3862  nnmordi  6583  omnimkv  7231  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  facdiv  10847  facwordi  10849  bezoutlemmain  12190  bezoutlemaz  12195  bezoutlembz  12196  algcvgblem  12242  prmfac1  12345  infpnlem1  12553  cncfco  14911  limccnpcntop  14995  limccoap  14998  bj-rspgt  15516