Theorem imim2d 54

Description: Deduction adding nested antecedents. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
imim2d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imim2d	⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

Proof of Theorem imim2d

Step	Hyp	Ref	Expression
1		imim2d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3	2	a2d 26	1 ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

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  3846  nnmordi  6536  omnimkv  7179  caucvgsrlemoffcau  7822  caucvgsrlemoffres  7824  facdiv  10745  facwordi  10747  bezoutlemmain  12026  bezoutlemaz  12031  bezoutlembz  12032  algcvgblem  12076  prmfac1  12179  infpnlem1  12386  cncfco  14515  limccnpcntop  14581  limccoap  14584  bj-rspgt  14975