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  7864  fzind  9763  exbtwnzlemshrink  10685  rebtwn2zlemshrink  10690  seq3fveq2  10914  seqfveq2g  10916  seq3shft2  10920  seqshft2g  10921  monoord  10924  seq3split  10927  seqsplitg  10928  seq3id2  10965  seqhomog  10969  seq3coll  11296  rexico  11989  cnntr  15328  bcmono  16124  2sqlem6  16251  eupth2lemsfi  16731  setindft  17003