Theorem imim2d 53

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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  imim2  54  embantd  55  imim12d  73  anc2r  321  pm5.31  340  con4biddc  788  jaddc  795  hbimd  1506  19.21ht  1514  nfimd  1518  19.23t  1608  spimth  1665  ssuni  3649  nnmordi  6205  caucvgsrlemoffcau  7246  caucvgsrlemoffres  7248  facdiv  9981  facwordi  9983  bezoutlemmain  10767  bezoutlemaz  10772  bezoutlembz  10773  algcvgblem  10811  prmfac1  10911  bj-rspgt  11029