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  12034  lediv23  12035  divalglem8  16329  isdrngd  20668  isdrngdOLD  20670  deg1tm  26040  ax5seglem1  28891  ax5seglem2  28892  nvaddsub4  30619  nmoub2i  30736  cdleme21at  40307  cdleme42f  40459  trlcoabs2N  40701  tendoplcl2  40757  tendopltp  40759  cdlemk2  40811  cdlemk8  40817  cdlemk9  40818  cdlemk9bN  40819  cdleml8  40962  dihglblem3N  41274  dihglblem3aN  41275  fourierdlem42  46131  lincscm  48416  itsclc0yqsol  48750