Theorem 3adant2r 1198

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ltdiv23  12107  lediv23  12108  divalglem8  16459  isdrngd  20850  isdrngdOLD  20852  deg1tm  26257  ax5seglem1  29256  ax5seglem2  29257  nvaddsub4  30987  nmoub2i  31104  eldisjs6  39567  cdleme21at  41080  cdleme42f  41232  trlcoabs2N  41474  tendoplcl2  41530  tendopltp  41532  cdlemk2  41584  cdlemk8  41590  cdlemk9  41591  cdlemk9bN  41592  cdleml8  41735  dihglblem3N  42047  dihglblem3aN  42048  fourierdlem42  46843  lincscm  49187  itsclc0yqsol  49521