Theorem 3adant2r 1192

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ltdiv23  12080  lediv23  12081  divalglem8  16417  isdrngd  20794  isdrngdOLD  20796  deg1tm  26159  ax5seglem1  29075  ax5seglem2  29076  nvaddsub4  30806  nmoub2i  30923  eldisjs6  39403  cdleme21at  40916  cdleme42f  41068  trlcoabs2N  41310  tendoplcl2  41366  tendopltp  41368  cdlemk2  41420  cdlemk8  41426  cdlemk9  41427  cdlemk9bN  41428  cdleml8  41571  dihglblem3N  41883  dihglblem3aN  41884  fourierdlem42  46687  lincscm  49016  itsclc0yqsol  49350