Theorem 3adant1l 1195

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant1l	⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant1l

Step	Hyp	Ref	Expression
1		simpr 489	. 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an1 1181	1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ad5ant245  1384  cfsmolem  10255  axdc3lem4  10438  issubmnd  18820  mhmima  18885  rhmimasubrng  20652  maducoeval2  22778  cramerlem3  22827  restnlly  23620  efgh  26684  hasheuni  34453  matunitlindflem1  38245  pellex  43542  mendlmod  43896  disjf1o  45889  ssfiunibd  46008  mullimc  46312  mullimcf  46319  limclner  46345  limsupresxr  46460  liminfresxr  46461  sge0lefi  47092  isomenndlem  47224  hoicvr  47242  ovncvrrp  47258