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  861  jaddc  868  hbimd  1599  19.21ht  1607  nfimd  1611  19.23t  1703  spimth  1761  ssuni  3889  nnmordi  6632  omnimkv  7291  caucvgsrlemoffcau  7953  caucvgsrlemoffres  7955  facdiv  10927  facwordi  10929  bezoutlemmain  12485  bezoutlemaz  12490  bezoutlembz  12491  algcvgblem  12537  prmfac1  12640  infpnlem1  12848  mplsubgfileminv  14629  cncfco  15230  limccnpcntop  15314  limccoap  15317  bj-rspgt  16060