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  1595  19.21ht  1603  nfimd  1607  19.23t  1699  spimth  1757  ssuni  3871  nnmordi  6601  omnimkv  7257  caucvgsrlemoffcau  7910  caucvgsrlemoffres  7912  facdiv  10881  facwordi  10883  bezoutlemmain  12261  bezoutlemaz  12266  bezoutlembz  12267  algcvgblem  12313  prmfac1  12416  infpnlem1  12624  mplsubgfileminv  14404  cncfco  15005  limccnpcntop  15089  limccoap  15092  bj-rspgt  15655