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  1584  19.21ht  1592  nfimd  1596  19.23t  1688  spimth  1746  ssuni  3858  nnmordi  6571  omnimkv  7217  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  facdiv  10812  facwordi  10814  bezoutlemmain  12138  bezoutlemaz  12143  bezoutlembz  12144  algcvgblem  12190  prmfac1  12293  infpnlem1  12500  cncfco  14770  limccnpcntop  14854  limccoap  14857  bj-rspgt  15348