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  12045  lediv23  12046  divalglem8  16339  isdrngd  20710  isdrngdOLD  20712  deg1tm  26092  ax5seglem1  29013  ax5seglem2  29014  nvaddsub4  30744  nmoub2i  30861  eldisjs6  39185  cdleme21at  40698  cdleme42f  40850  trlcoabs2N  41092  tendoplcl2  41148  tendopltp  41150  cdlemk2  41202  cdlemk8  41208  cdlemk9  41209  cdlemk9bN  41210  cdleml8  41353  dihglblem3N  41665  dihglblem3aN  41666  fourierdlem42  46501  lincscm  48784  itsclc0yqsol  49118