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  230  expt  647  hbimd  1553  moim  2064  moimv  2066  sstr2  3109  ssralv  3166  soss  4244  nneneq  6759  prarloclem3  7329  fzind  9190  exbtwnzlemshrink  10057  rebtwn2zlemshrink  10062  seq3fveq2  10273  seq3shft2  10277  monoord  10280  seq3split  10283  seq3id2  10313  seq3coll  10617  rexico  11025  cnntr  12433  setindft  13334