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  663  hbimd  1622  moim  2144  moimv  2146  sstr2  3235  ssralv  3292  soss  4417  nneneq  7086  prarloclem3  7760  fzind  9638  exbtwnzlemshrink  10552  rebtwn2zlemshrink  10557  seq3fveq2  10781  seqfveq2g  10783  seq3shft2  10787  seqshft2g  10788  monoord  10791  seq3split  10794  seqsplitg  10795  seq3id2  10832  seqhomog  10836  seq3coll  11150  rexico  11842  cnntr  15016  2sqlem6  15919  eupth2lemsfi  16399  setindft  16661