Theorem 3adant1l 1195

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ad5ant245  1384  cfsmolem  10276  axdc3lem4  10459  issubmnd  18872  mhmima  18940  rhmimasubrng  20734  maducoeval2  22868  matunitlindflem1  22907  cramerlem3  22920  restnlly  23714  efgh  26786  hasheuni  34603  pellex  43684  mendlmod  44038  disjf1o  46031  ssfiunibd  46150  mullimc  46454  mullimcf  46461  limclner  46487  limsupresxr  46602  liminfresxr  46603  sge0lefi  47234  isomenndlem  47366  hoicvr  47384  ovncvrrp  47400