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  326  pm5.31  346  con4biddc  847  jaddc  854  hbimd  1560  19.21ht  1568  nfimd  1572  19.23t  1664  spimth  1722  ssuni  3805  nnmordi  6475  omnimkv  7111  caucvgsrlemoffcau  7730  caucvgsrlemoffres  7732  facdiv  10640  facwordi  10642  bezoutlemmain  11916  bezoutlemaz  11921  bezoutlembz  11922  algcvgblem  11960  prmfac1  12061  cncfco  13119  limccnpcntop  13185  limccoap  13188  bj-rspgt  13502