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  869  jaddc  876  hbimd  1626  19.21ht  1634  nfimd  1638  19.23t  1729  spimth  1788  ssuni  3955  nnmordi  6783  omnimkv  7490  caucvgsrlemoffcau  8159  caucvgsrlemoffres  8161  facdiv  11159  facwordi  11161  bezoutlemmain  12758  bezoutlemaz  12763  bezoutlembz  12764  algcvgblem  12810  prmfac1  12913  infpnlem1  13121  mplsubgfileminv  15074  cncfco  15675  limccnpcntop  15759  limccoap  15762  bj-rspgt  16797