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  12038  lediv23  12039  divalglem8  16360  isdrngd  20733  isdrngdOLD  20735  deg1tm  26094  ax5seglem1  29011  ax5seglem2  29012  nvaddsub4  30743  nmoub2i  30860  eldisjs6  39275  cdleme21at  40788  cdleme42f  40940  trlcoabs2N  41182  tendoplcl2  41238  tendopltp  41240  cdlemk2  41292  cdlemk8  41298  cdlemk9  41299  cdlemk9bN  41300  cdleml8  41443  dihglblem3N  41755  dihglblem3aN  41756  fourierdlem42  46595  lincscm  48918  itsclc0yqsol  49252