Theorem 3adant1l 1177

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ad5ant245  1363  cfsmolem  10310  axdc3lem4  10493  issubmnd  18774  mhmima  18838  rhmimasubrng  20566  maducoeval2  22646  cramerlem3  22695  restnlly  23490  efgh  26583  hasheuni  34086  matunitlindflem1  37623  pellex  42846  mendlmod  43201  disjf1o  45196  ssfiunibd  45321  mullimc  45631  mullimcf  45638  limclner  45666  limsupresxr  45781  liminfresxr  45782  sge0lefi  46413  isomenndlem  46545  hoicvr  46563  ovncvrrp  46579