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  862  jaddc  869  hbimd  1619  19.21ht  1627  nfimd  1631  19.23t  1723  spimth  1781  ssuni  3913  nnmordi  6679  omnimkv  7346  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  facdiv  10990  facwordi  10992  bezoutlemmain  12559  bezoutlemaz  12564  bezoutlembz  12565  algcvgblem  12611  prmfac1  12714  infpnlem1  12922  mplsubgfileminv  14704  cncfco  15305  limccnpcntop  15389  limccoap  15392  bj-rspgt  16318