Theorem 3adant2r 1196

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  ltdiv23  12097  lediv23  12098  divalglem8  16448  isdrngd  20838  isdrngdOLD  20840  deg1tm  26237  ax5seglem1  29187  ax5seglem2  29188  nvaddsub4  30918  nmoub2i  31035  eldisjs6  39451  cdleme21at  40964  cdleme42f  41116  trlcoabs2N  41358  tendoplcl2  41414  tendopltp  41416  cdlemk2  41468  cdlemk8  41474  cdlemk9  41475  cdlemk9bN  41476  cdleml8  41619  dihglblem3N  41931  dihglblem3aN  41932  fourierdlem42  46721  lincscm  49061  itsclc0yqsol  49395