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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  ad5ant245  1362  cfsmolem  10261  axdc3lem4  10444  issubmnd  18648  mhmima  18702  maducoeval2  22124  cramerlem3  22173  restnlly  22968  efgh  26032  hasheuni  33021  matunitlindflem1  36422  pellex  41506  mendlmod  41868  disjf1o  43822  ssfiunibd  43954  mullimc  44267  mullimcf  44274  limclner  44302  limsupresxr  44417  liminfresxr  44418  sge0lefi  45049  isomenndlem  45181  hoicvr  45199  ovncvrrp  45215  rhmimasubrng  46678