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 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1  76  imbi1d  231  expt  667  hbimd  1626  moim  2151  moimv  2153  sstr2  3255  ssralv  3312  soss  4459  nneneq  7158  prarloclem3  7865  fzind  9766  exbtwnzlemshrink  10694  rebtwn2zlemshrink  10699  seq3fveq2  10926  seqfveq2g  10928  seq3shft2  10932  seqshft2g  10933  monoord  10936  seq3split  10939  seqsplitg  10940  seq3id2  10977  seqhomog  10981  seq3coll  11309  rexico  12003  cnntr  15378  bcmono  16226  2sqlem6  16361  eupth2lemsfi  16841  setindft  17113