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  3849  nnmordi  6545  omnimkv  7189  caucvgsrlemoffcau  7832  caucvgsrlemoffres  7834  facdiv  10759  facwordi  10761  bezoutlemmain  12040  bezoutlemaz  12045  bezoutlembz  12046  algcvgblem  12092  prmfac1  12195  infpnlem1  12402  cncfco  14563  limccnpcntop  14629  limccoap  14632  bj-rspgt  15024