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  787  jaddc  794  hbimd  1505  19.21ht  1513  nfimd  1517  19.23t  1607  spimth  1663  ssuni  3623  nnmordi  6112  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  facdiv  9665  facwordi  9667  bezoutlemmain  10387  bezoutlemaz  10392  bezoutlembz  10393  algcvgblem  10431  prmfac1  10531  bj-rspgt  10596