Theorem 3adant2r 1184

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  ltdiv23  11268  lediv23  11269  divalglem8  15530  isdrngd  19164  deg1tm  24315  ax5seglem1  26277  ax5seglem2  26278  nvaddsub4  28098  nmoub2i  28215  cdleme21at  36476  cdleme42f  36628  trlcoabs2N  36870  tendoplcl2  36926  tendopltp  36928  cdlemk2  36980  cdlemk8  36986  cdlemk9  36987  cdlemk9bN  36988  cdleml8  37131  dihglblem3N  37443  dihglblem3aN  37444  fourierdlem42  41285  lincscm  43226  itsclc0yqsol  43492