Theorem 3adant2r 1178

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ltdiv23  11866  lediv23  11867  divalglem8  16109  isdrngd  20016  deg1tm  25283  ax5seglem1  27296  ax5seglem2  27297  nvaddsub4  29019  nmoub2i  29136  cdleme21at  38342  cdleme42f  38494  trlcoabs2N  38736  tendoplcl2  38792  tendopltp  38794  cdlemk2  38846  cdlemk8  38852  cdlemk9  38853  cdlemk9bN  38854  cdleml8  38997  dihglblem3N  39309  dihglblem3aN  39310  fourierdlem42  43690  lincscm  45771  itsclc0yqsol  46110