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  1587  19.21ht  1595  nfimd  1599  19.23t  1691  spimth  1749  ssuni  3862  nnmordi  6583  omnimkv  7231  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  facdiv  10849  facwordi  10851  bezoutlemmain  12192  bezoutlemaz  12197  bezoutlembz  12198  algcvgblem  12244  prmfac1  12347  infpnlem1  12555  mplsubgfileminv  14334  cncfco  14935  limccnpcntop  15019  limccoap  15022  bj-rspgt  15540