Theorem 3adant1l 1175

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 1162	1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1088

This theorem is referenced by:  ad5ant245  1360  cfsmolem  10026  axdc3lem4  10209  issubmnd  18412  maducoeval2  21789  cramerlem3  21838  restnlly  22633  efgh  25697  hasheuni  32053  matunitlindflem1  35773  pellex  40657  mendlmod  41018  disjf1o  42729  ssfiunibd  42848  mullimc  43157  mullimcf  43164  limclner  43192  limsupresxr  43307  liminfresxr  43308  sge0lefi  43936  isomenndlem  44068  hoicvr  44086  ovncvrrp  44102