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 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  12126  lediv23  12127  divalglem8  16406  isdrngd  20712  isdrngdOLD  20714  deg1tm  26063  ax5seglem1  28841  ax5seglem2  28842  nvaddsub4  30572  nmoub2i  30689  cdleme21at  40276  cdleme42f  40428  trlcoabs2N  40670  tendoplcl2  40726  tendopltp  40728  cdlemk2  40780  cdlemk8  40786  cdlemk9  40787  cdlemk9bN  40788  cdleml8  40931  dihglblem3N  41243  dihglblem3aN  41244  fourierdlem42  46114  lincscm  48300  itsclc0yqsol  48638