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  1584  19.21ht  1592  nfimd  1596  19.23t  1688  spimth  1746  ssuni  3857  nnmordi  6569  omnimkv  7215  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  facdiv  10809  facwordi  10811  bezoutlemmain  12135  bezoutlemaz  12140  bezoutlembz  12141  algcvgblem  12187  prmfac1  12290  infpnlem1  12497  cncfco  14746  limccnpcntop  14829  limccoap  14832  bj-rspgt  15278