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  865  jaddc  872  hbimd  1622  19.21ht  1630  nfimd  1634  19.23t  1725  spimth  1784  ssuni  3941  nnmordi  6762  omnimkv  7460  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  facdiv  11128  facwordi  11130  bezoutlemmain  12722  bezoutlemaz  12727  bezoutlembz  12728  algcvgblem  12774  prmfac1  12877  infpnlem1  13085  mplsubgfileminv  14984  cncfco  15585  limccnpcntop  15669  limccoap  15672  bj-rspgt  16697