Theorem 3adant2r 1180

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 484	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an2 1165	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  ltdiv23  12105  lediv23  12106  divalglem8  16343  isdrngd  20390  isdrngdOLD  20392  deg1tm  25636  ax5seglem1  28186  ax5seglem2  28187  nvaddsub4  29910  nmoub2i  30027  cdleme21at  39199  cdleme42f  39351  trlcoabs2N  39593  tendoplcl2  39649  tendopltp  39651  cdlemk2  39703  cdlemk8  39709  cdlemk9  39710  cdlemk9bN  39711  cdleml8  39854  dihglblem3N  40166  dihglblem3aN  40167  fourierdlem42  44865  lincscm  47111  itsclc0yqsol  47450