Theorem 3adant1l 1189

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ad5ant245  1375  cfsmolem  10224  axdc3lem4  10407  issubmnd  18778  mhmima  18842  rhmimasubrng  20595  maducoeval2  22680  cramerlem3  22729  restnlly  23522  efgh  26583  hasheuni  34343  matunitlindflem1  38079  pellex  43376  mendlmod  43730  disjf1o  45733  ssfiunibd  45852  mullimc  46156  mullimcf  46163  limclner  46189  limsupresxr  46304  liminfresxr  46305  sge0lefi  46936  isomenndlem  47068  hoicvr  47086  ovncvrrp  47102