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  10168  axdc3lem4  10351  issubmnd  18671  mhmima  18735  rhmimasubrng  20483  maducoeval2  22556  cramerlem3  22605  restnlly  23398  efgh  26478  hasheuni  34119  matunitlindflem1  37676  pellex  42952  mendlmod  43306  disjf1o  45312  ssfiunibd  45434  mullimc  45740  mullimcf  45747  limclner  45773  limsupresxr  45888  liminfresxr  45889  sge0lefi  46520  isomenndlem  46652  hoicvr  46670  ovncvrrp  46686