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  10267  axdc3lem4  10450  issubmnd  18686  mhmima  18742  rhmimasubrng  20454  maducoeval2  22362  cramerlem3  22411  restnlly  23206  efgh  26274  hasheuni  33369  matunitlindflem1  36787  pellex  41875  mendlmod  42237  disjf1o  44189  ssfiunibd  44318  mullimc  44631  mullimcf  44638  limclner  44666  limsupresxr  44781  liminfresxr  44782  sge0lefi  45413  isomenndlem  45545  hoicvr  45563  ovncvrrp  45579