Theorem 3adant2r 1176

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  ltdiv23  11520  lediv23  11521  divalglem8  15741  isdrngd  19520  deg1tm  24719  ax5seglem1  26722  ax5seglem2  26723  nvaddsub4  28440  nmoub2i  28557  cdleme21at  37624  cdleme42f  37776  trlcoabs2N  38018  tendoplcl2  38074  tendopltp  38076  cdlemk2  38128  cdlemk8  38134  cdlemk9  38135  cdlemk9bN  38136  cdleml8  38279  dihglblem3N  38591  dihglblem3aN  38592  fourierdlem42  42791  lincscm  44839  itsclc0yqsol  45178