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 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1  76  imbi1d  231  expt  667  hbimd  1626  moim  2151  moimv  2153  sstr2  3255  ssralv  3312  soss  4461  nneneq  7163  prarloclem3  7871  fzind  9773  exbtwnzlemshrink  10701  rebtwn2zlemshrink  10706  seq3fveq2  10934  seqfveq2g  10936  seq3shft2  10940  seqshft2g  10941  monoord  10944  seq3split  10947  seqsplitg  10948  seq3id2  10985  seqhomog  10989  seq3coll  11317  rexico  12011  cnntr  15463  bcmono  16316  2sqlem6  16456  eupth2lemsfi  16936  setindft  17208