Theorem 3adant1l 1175

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 1162	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  1360  cfsmolem  10307  axdc3lem4  10490  issubmnd  18786  mhmima  18850  rhmimasubrng  20582  maducoeval2  22661  cramerlem3  22710  restnlly  23505  efgh  26597  hasheuni  34065  matunitlindflem1  37602  pellex  42822  mendlmod  43177  disjf1o  45133  ssfiunibd  45259  mullimc  45571  mullimcf  45578  limclner  45606  limsupresxr  45721  liminfresxr  45722  sge0lefi  46353  isomenndlem  46485  hoicvr  46503  ovncvrrp  46519