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  3861  nnmordi  6574  omnimkv  7222  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  facdiv  10830  facwordi  10832  bezoutlemmain  12165  bezoutlemaz  12170  bezoutlembz  12171  algcvgblem  12217  prmfac1  12320  infpnlem1  12528  cncfco  14827  limccnpcntop  14911  limccoap  14914  bj-rspgt  15432