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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ltdiv23  12211  lediv23  12212  divalglem8  16575  isdrngd  21027  isdrngdOLD  21029  deg1tm  26442  ax5seglem1  29511  ax5seglem2  29512  nvaddsub4  31264  nmoub2i  31381  eldisjs6  39965  cdleme21at  41478  cdleme42f  41630  trlcoabs2N  41872  tendoplcl2  41928  tendopltp  41930  cdlemk2  41982  cdlemk8  41988  cdlemk9  41989  cdlemk9bN  41990  cdleml8  42133  dihglblem3N  42445  dihglblem3aN  42446  fourierdlem42  47252  lincscm  49635  itsclc0yqsol  49969