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  3881  nnmordi  6620  omnimkv  7279  caucvgsrlemoffcau  7941  caucvgsrlemoffres  7943  facdiv  10915  facwordi  10917  bezoutlemmain  12404  bezoutlemaz  12409  bezoutlembz  12410  algcvgblem  12456  prmfac1  12559  infpnlem1  12767  mplsubgfileminv  14547  cncfco  15148  limccnpcntop  15232  limccoap  15235  bj-rspgt  15892