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  857  jaddc  864  hbimd  1573  19.21ht  1581  nfimd  1585  19.23t  1677  spimth  1735  ssuni  3832  nnmordi  6517  omnimkv  7154  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  facdiv  10718  facwordi  10720  bezoutlemmain  11999  bezoutlemaz  12004  bezoutlembz  12005  algcvgblem  12049  prmfac1  12152  infpnlem1  12357  cncfco  14081  limccnpcntop  14147  limccoap  14150  bj-rspgt  14541