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  864  jaddc  871  hbimd  1621  19.21ht  1629  nfimd  1633  19.23t  1724  spimth  1782  ssuni  3916  nnmordi  6689  omnimkv  7360  caucvgsrlemoffcau  8023  caucvgsrlemoffres  8025  facdiv  11006  facwordi  11008  bezoutlemmain  12592  bezoutlemaz  12597  bezoutlembz  12598  algcvgblem  12644  prmfac1  12747  infpnlem1  12955  mplsubgfileminv  14743  cncfco  15344  limccnpcntop  15428  limccoap  15431  bj-rspgt  16443