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  659  hbimd  1597  moim  2119  moimv  2121  sstr2  3204  ssralv  3261  soss  4368  nneneq  6968  prarloclem3  7625  fzind  9503  exbtwnzlemshrink  10408  rebtwn2zlemshrink  10413  seq3fveq2  10637  seqfveq2g  10639  seq3shft2  10643  seqshft2g  10644  monoord  10647  seq3split  10650  seqsplitg  10651  seq3id2  10688  seqhomog  10692  seq3coll  11004  rexico  11602  cnntr  14767  2sqlem6  15667  setindft  16035