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  3191  ssralv  3248  soss  4350  nneneq  6927  prarloclem3  7583  fzind  9460  exbtwnzlemshrink  10357  rebtwn2zlemshrink  10362  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  seq3id2  10637  seqhomog  10641  seq3coll  10953  rexico  11405  cnntr  14569  2sqlem6  15469  setindft  15719