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  1725  spimth  1783  ssuni  3915  nnmordi  6684  omnimkv  7355  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  facdiv  11001  facwordi  11003  bezoutlemmain  12571  bezoutlemaz  12576  bezoutlembz  12577  algcvgblem  12623  prmfac1  12726  infpnlem1  12934  mplsubgfileminv  14717  cncfco  15318  limccnpcntop  15402  limccoap  15405  bj-rspgt  16403