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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ltdiv23  12074  lediv23  12075  divalglem8  16370  isdrngd  20674  isdrngdOLD  20676  deg1tm  26024  ax5seglem1  28855  ax5seglem2  28856  nvaddsub4  30586  nmoub2i  30703  cdleme21at  40322  cdleme42f  40474  trlcoabs2N  40716  tendoplcl2  40772  tendopltp  40774  cdlemk2  40826  cdlemk8  40832  cdlemk9  40833  cdlemk9bN  40834  cdleml8  40977  dihglblem3N  41289  dihglblem3aN  41290  fourierdlem42  46147  lincscm  48416  itsclc0yqsol  48750