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  847  jaddc  854  hbimd  1561  19.21ht  1569  nfimd  1573  19.23t  1665  spimth  1723  ssuni  3811  nnmordi  6484  omnimkv  7120  caucvgsrlemoffcau  7739  caucvgsrlemoffres  7741  facdiv  10651  facwordi  10653  bezoutlemmain  11931  bezoutlemaz  11936  bezoutlembz  11937  algcvgblem  11981  prmfac1  12084  infpnlem1  12289  cncfco  13228  limccnpcntop  13294  limccoap  13297  bj-rspgt  13677