Theorem 3adant1l 1177

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ad5ant245  1363  cfsmolem  10180  axdc3lem4  10363  issubmnd  18686  mhmima  18750  rhmimasubrng  20499  maducoeval2  22584  cramerlem3  22633  restnlly  23426  efgh  26506  hasheuni  34242  matunitlindflem1  37813  pellex  43073  mendlmod  43427  disjf1o  45431  ssfiunibd  45553  mullimc  45858  mullimcf  45865  limclner  45891  limsupresxr  46006  liminfresxr  46007  sge0lefi  46638  isomenndlem  46770  hoicvr  46788  ovncvrrp  46804