Theorem imim1d 74

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

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  imim1  75  imbi1d  229  expt  615  hbimd  1505  moim  2005  moimv  2007  sstr2  3006  ssralv  3058  soss  4069  nneneq  6343  prarloclem3  6687  fzind  8462  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  rexico  10107  setindft  10760