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  12235  lediv23  12236  divalglem8  16599  isdrngd  21052  isdrngdOLD  21054  deg1tm  26467  ax5seglem1  29536  ax5seglem2  29537  nvaddsub4  31289  nmoub2i  31406  eldisjs6  40064  cdleme21at  41577  cdleme42f  41729  trlcoabs2N  41971  tendoplcl2  42027  tendopltp  42029  cdlemk2  42081  cdlemk8  42087  cdlemk9  42088  cdlemk9bN  42089  cdleml8  42232  dihglblem3N  42544  dihglblem3aN  42545  fourierdlem42  47364  lincscm  49747  itsclc0yqsol  50081