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  10272  axdc3lem4  10455  issubmnd  18848  mhmima  18915  rhmimasubrng  20702  maducoeval2  22834  cramerlem3  22883  restnlly  23676  efgh  26743  hasheuni  34506  matunitlindflem1  38308  pellex  43603  mendlmod  43957  disjf1o  45950  ssfiunibd  46069  mullimc  46373  mullimcf  46380  limclner  46406  limsupresxr  46521  liminfresxr  46522  sge0lefi  47153  isomenndlem  47285  hoicvr  47303  ovncvrrp  47319