Theorem 3adant1l 1176

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  ad5ant245  1361  cfsmolem  10215  axdc3lem4  10398  issubmnd  18597  maducoeval2  22026  cramerlem3  22075  restnlly  22870  efgh  25934  hasheuni  32773  matunitlindflem1  36147  pellex  41216  mendlmod  41578  disjf1o  43532  ssfiunibd  43664  mullimc  43977  mullimcf  43984  limclner  44012  limsupresxr  44127  liminfresxr  44128  sge0lefi  44759  isomenndlem  44891  hoicvr  44909  ovncvrrp  44925