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  658  hbimd  1587  moim  2109  moimv  2111  sstr2  3190  ssralv  3247  soss  4349  nneneq  6918  prarloclem3  7564  fzind  9441  exbtwnzlemshrink  10338  rebtwn2zlemshrink  10343  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord  10577  seq3split  10580  seqsplitg  10581  seq3id2  10618  seqhomog  10622  seq3coll  10934  rexico  11386  cnntr  14461  2sqlem6  15361  setindft  15611