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  2145  moimv  2147  sstr2  3244  ssralv  3301  soss  4434  nneneq  7110  prarloclem3  7811  fzind  9692  exbtwnzlemshrink  10607  rebtwn2zlemshrink  10612  seq3fveq2  10836  seqfveq2g  10838  seq3shft2  10842  seqshft2g  10843  monoord  10846  seq3split  10849  seqsplitg  10850  seq3id2  10887  seqhomog  10891  seq3coll  11210  rexico  11902  cnntr  15082  2sqlem6  15985  eupth2lemsfi  16465  setindft  16727