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  12160  lediv23  12161  divalglem8  16438  isdrngd  20766  isdrngdOLD  20768  deg1tm  26159  ax5seglem1  28944  ax5seglem2  28945  nvaddsub4  30677  nmoub2i  30794  cdleme21at  40331  cdleme42f  40483  trlcoabs2N  40725  tendoplcl2  40781  tendopltp  40783  cdlemk2  40835  cdlemk8  40841  cdlemk9  40842  cdlemk9bN  40843  cdleml8  40986  dihglblem3N  41298  dihglblem3aN  41299  fourierdlem42  46169  lincscm  48352  itsclc0yqsol  48690