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

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  ltdiv23  12109  lediv23  12110  divalglem8  16347  isdrngd  20533  isdrngdOLD  20535  deg1tm  25871  ax5seglem1  28453  ax5seglem2  28454  nvaddsub4  30177  nmoub2i  30294  cdleme21at  39502  cdleme42f  39654  trlcoabs2N  39896  tendoplcl2  39952  tendopltp  39954  cdlemk2  40006  cdlemk8  40012  cdlemk9  40013  cdlemk9bN  40014  cdleml8  40157  dihglblem3N  40469  dihglblem3aN  40470  fourierdlem42  45163  lincscm  47198  itsclc0yqsol  47537