Theorem 3adant2r 1179

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant2r	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant2r

Step	Hyp	Ref	Expression
1		simpl 483	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an2 1164	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089

This theorem is referenced by:  ltdiv23  12101  lediv23  12102  divalglem8  16339  isdrngd  20340  isdrngdOLD  20342  deg1tm  25627  ax5seglem1  28175  ax5seglem2  28176  nvaddsub4  29897  nmoub2i  30014  cdleme21at  39187  cdleme42f  39339  trlcoabs2N  39581  tendoplcl2  39637  tendopltp  39639  cdlemk2  39691  cdlemk8  39697  cdlemk9  39698  cdlemk9bN  39699  cdleml8  39842  dihglblem3N  40154  dihglblem3aN  40155  fourierdlem42  44851  lincscm  47064  itsclc0yqsol  47403