Theorem 3adant1l 1172

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ad5ant245  1357  cfsmolem  9686  axdc3lem4  9869  issubmnd  17932  maducoeval2  21243  cramerlem3  21292  restnlly  22084  efgh  25119  hasheuni  31339  matunitlindflem1  34882  pellex  39425  mendlmod  39786  disjf1o  41444  ssfiunibd  41568  mullimc  41889  mullimcf  41896  limclner  41924  limsupresxr  42039  liminfresxr  42040  sge0lefi  42673  isomenndlem  42805  hoicvr  42823  ovncvrrp  42839