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  859  jaddc  866  hbimd  1597  19.21ht  1605  nfimd  1609  19.23t  1701  spimth  1759  ssuni  3886  nnmordi  6625  omnimkv  7284  caucvgsrlemoffcau  7946  caucvgsrlemoffres  7948  facdiv  10920  facwordi  10922  bezoutlemmain  12434  bezoutlemaz  12439  bezoutlembz  12440  algcvgblem  12486  prmfac1  12589  infpnlem1  12797  mplsubgfileminv  14577  cncfco  15178  limccnpcntop  15262  limccoap  15265  bj-rspgt  15922