Theorem 3adant2r 1177

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 1162	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ltdiv23  11796  lediv23  11797  divalglem8  16037  isdrngd  19931  deg1tm  25188  ax5seglem1  27199  ax5seglem2  27200  nvaddsub4  28920  nmoub2i  29037  cdleme21at  38269  cdleme42f  38421  trlcoabs2N  38663  tendoplcl2  38719  tendopltp  38721  cdlemk2  38773  cdlemk8  38779  cdlemk9  38780  cdlemk9bN  38781  cdleml8  38924  dihglblem3N  39236  dihglblem3aN  39237  fourierdlem42  43580  lincscm  45659  itsclc0yqsol  45998