Theorem 3adant2r 1175

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 485	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an2 1160	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ltdiv23  11525  lediv23  11526  divalglem8  15745  isdrngd  19521  deg1tm  24706  ax5seglem1  26708  ax5seglem2  26709  nvaddsub4  28428  nmoub2i  28545  cdleme21at  37458  cdleme42f  37610  trlcoabs2N  37852  tendoplcl2  37908  tendopltp  37910  cdlemk2  37962  cdlemk8  37968  cdlemk9  37969  cdlemk9bN  37970  cdleml8  38113  dihglblem3N  38425  dihglblem3aN  38426  fourierdlem42  42427  lincscm  44478  itsclc0yqsol  44744