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  862  jaddc  869  hbimd  1619  19.21ht  1627  nfimd  1631  19.23t  1723  spimth  1781  ssuni  3913  nnmordi  6679  omnimkv  7349  caucvgsrlemoffcau  8011  caucvgsrlemoffres  8013  facdiv  10993  facwordi  10995  bezoutlemmain  12562  bezoutlemaz  12567  bezoutlembz  12568  algcvgblem  12614  prmfac1  12717  infpnlem1  12925  mplsubgfileminv  14707  cncfco  15308  limccnpcntop  15392  limccoap  15395  bj-rspgt  16332