Theorem 3adant2r 1186

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ltdiv23  12045  lediv23  12046  divalglem8  16367  isdrngd  20744  isdrngdOLD  20746  deg1tm  26109  ax5seglem1  29022  ax5seglem2  29023  nvaddsub4  30753  nmoub2i  30870  eldisjs6  39314  cdleme21at  40827  cdleme42f  40979  trlcoabs2N  41221  tendoplcl2  41277  tendopltp  41279  cdlemk2  41331  cdlemk8  41337  cdlemk9  41338  cdlemk9bN  41339  cdleml8  41482  dihglblem3N  41794  dihglblem3aN  41795  fourierdlem42  46599  lincscm  48928  itsclc0yqsol  49262