Theorem 3adant2r 1198

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ltdiv23  12134  lediv23  12135  divalglem8  16496  isdrngd  20937  isdrngdOLD  20939  deg1tm  26351  ax5seglem1  29393  ax5seglem2  29394  nvaddsub4  31146  nmoub2i  31263  eldisjs6  39696  cdleme21at  41209  cdleme42f  41361  trlcoabs2N  41603  tendoplcl2  41659  tendopltp  41661  cdlemk2  41713  cdlemk8  41719  cdlemk9  41720  cdlemk9bN  41721  cdleml8  41864  dihglblem3N  42176  dihglblem3aN  42177  fourierdlem42  46985  lincscm  49368  itsclc0yqsol  49702