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  10351  axdc3lem4  10534  issubmnd  18958  mhmima  19026  rhmimasubrng  20823  maducoeval2  22960  matunitlindflem1  22999  cramerlem3  23012  restnlly  23806  efgh  26874  hasheuni  34763  pellex  43935  mendlmod  44284  disjf1o  46299  ssfiunibd  46418  mullimc  46721  mullimcf  46728  limclner  46754  limsupresxr  46869  liminfresxr  46870  sge0lefi  47501  isomenndlem  47633  hoicvr  47651  ovncvrrp  47667