Theorem 3adant2r 1179

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 1164	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  12186  lediv23  12187  divalglem8  16448  isdrngd  20787  isdrngdOLD  20789  deg1tm  26178  ax5seglem1  28961  ax5seglem2  28962  nvaddsub4  30689  nmoub2i  30806  cdleme21at  40285  cdleme42f  40437  trlcoabs2N  40679  tendoplcl2  40735  tendopltp  40737  cdlemk2  40789  cdlemk8  40795  cdlemk9  40796  cdlemk9bN  40797  cdleml8  40940  dihglblem3N  41252  dihglblem3aN  41253  fourierdlem42  46070  lincscm  48159  itsclc0yqsol  48498