Theorem 3adant2r 1178

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

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

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 1088

This theorem is referenced by:  ltdiv23  12157  lediv23  12158  divalglem8  16434  isdrngd  20782  isdrngdOLD  20784  deg1tm  26173  ax5seglem1  28958  ax5seglem2  28959  nvaddsub4  30686  nmoub2i  30803  cdleme21at  40311  cdleme42f  40463  trlcoabs2N  40705  tendoplcl2  40761  tendopltp  40763  cdlemk2  40815  cdlemk8  40821  cdlemk9  40822  cdlemk9bN  40823  cdleml8  40966  dihglblem3N  41278  dihglblem3aN  41279  fourierdlem42  46105  lincscm  48276  itsclc0yqsol  48614