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  2147  moimv  2149  sstr2  3249  ssralv  3306  soss  4440  nneneq  7124  prarloclem3  7828  fzind  9714  exbtwnzlemshrink  10635  rebtwn2zlemshrink  10640  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  seq3id2  10915  seqhomog  10919  seq3coll  11242  rexico  11935  cnntr  15220  2sqlem6  16123  eupth2lemsfi  16603  setindft  16875