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  657  hbimd  1573  moim  2090  moimv  2092  sstr2  3163  ssralv  3220  soss  4315  nneneq  6857  prarloclem3  7496  fzind  9368  exbtwnzlemshrink  10249  rebtwn2zlemshrink  10254  seq3fveq2  10469  seq3shft2  10473  monoord  10476  seq3split  10479  seq3id2  10509  seq3coll  10822  rexico  11230  cnntr  13728  2sqlem6  14470  setindft  14720