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  661  hbimd  1619  moim  2142  moimv  2144  sstr2  3231  ssralv  3288  soss  4402  nneneq  7006  prarloclem3  7672  fzind  9550  exbtwnzlemshrink  10455  rebtwn2zlemshrink  10460  seq3fveq2  10684  seqfveq2g  10686  seq3shft2  10690  seqshft2g  10691  monoord  10694  seq3split  10697  seqsplitg  10698  seq3id2  10735  seqhomog  10739  seq3coll  11051  rexico  11718  cnntr  14884  2sqlem6  15784  setindft  16258