Theorem 3adant1l 1193

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ad5ant245  1380  cfsmolem  10242  axdc3lem4  10425  issubmnd  18809  mhmima  18874  rhmimasubrng  20642  maducoeval2  22758  cramerlem3  22807  restnlly  23600  efgh  26664  hasheuni  34392  matunitlindflem1  38127  pellex  43424  mendlmod  43778  disjf1o  45767  ssfiunibd  45886  mullimc  46190  mullimcf  46197  limclner  46223  limsupresxr  46338  liminfresxr  46339  sge0lefi  46970  isomenndlem  47102  hoicvr  47120  ovncvrrp  47136