Theorem 3adant2r 1181

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 1165	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

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

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 1089

This theorem is referenced by:  ltdiv23  12047  lediv23  12048  divalglem8  16369  isdrngd  20742  isdrngdOLD  20744  deg1tm  26084  ax5seglem1  28997  ax5seglem2  28998  nvaddsub4  30728  nmoub2i  30845  eldisjs6  39261  cdleme21at  40774  cdleme42f  40926  trlcoabs2N  41168  tendoplcl2  41224  tendopltp  41226  cdlemk2  41278  cdlemk8  41284  cdlemk9  41285  cdlemk9bN  41286  cdleml8  41429  dihglblem3N  41741  dihglblem3aN  41742  fourierdlem42  46577  lincscm  48906  itsclc0yqsol  49240