Theorem imim1d 75

Description: Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)

Hypothesis

Ref	Expression
imim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imim1d	⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

Proof of Theorem imim1d

Step	Hyp	Ref	Expression
1		imim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 21	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	imim12d 74	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:  imim1  76  imbi1d  231  expt  657  hbimd  1573  moim  2090  moimv  2092  sstr2  3164  ssralv  3221  soss  4316  nneneq  6860  prarloclem3  7499  fzind  9371  exbtwnzlemshrink  10252  rebtwn2zlemshrink  10257  seq3fveq2  10472  seq3shft2  10476  monoord  10479  seq3split  10482  seq3id2  10512  seq3coll  10825  rexico  11233  cnntr  13886  2sqlem6  14628  setindft  14878