Theorem 3adant1l 1174

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 484	. 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an1 1161	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:  ad5ant245  1359  cfsmolem  9957  axdc3lem4  10140  issubmnd  18327  maducoeval2  21697  cramerlem3  21746  restnlly  22541  efgh  25602  hasheuni  31953  matunitlindflem1  35700  pellex  40573  mendlmod  40934  disjf1o  42618  ssfiunibd  42738  mullimc  43047  mullimcf  43054  limclner  43082  limsupresxr  43197  liminfresxr  43198  sge0lefi  43826  isomenndlem  43958  hoicvr  43976  ovncvrrp  43992