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  1385  cfsmolem  10375  axdc3lem4  10558  issubmnd  18982  mhmima  19050  rhmimasubrng  20848  maducoeval2  22985  matunitlindflem1  23024  cramerlem3  23037  restnlly  23831  efgh  26899  hasheuni  34787  pellex  44035  mendlmod  44383  disjf1o  46411  ssfiunibd  46530  mullimc  46833  mullimcf  46840  limclner  46866  limsupresxr  46981  liminfresxr  46982  sge0lefi  47613  isomenndlem  47745  hoicvr  47763  ovncvrrp  47779