Theorem imim2d 53

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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  imim2  54  embantd  55  imim12d  73  anc2r  321  pm5.31  340  con4biddc  792  jaddc  799  hbimd  1510  19.21ht  1518  nfimd  1522  19.23t  1612  spimth  1670  ssuni  3670  nnmordi  6255  caucvgsrlemoffcau  7322  caucvgsrlemoffres  7324  facdiv  10111  facwordi  10113  bezoutlemmain  11080  bezoutlemaz  11085  bezoutlembz  11086  algcvgblem  11124  prmfac1  11224  bj-rspgt  11343