Theorem 3adant1l 1178

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 1164	1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1089

This theorem is referenced by:  ad5ant245  1364  cfsmolem  10183  axdc3lem4  10366  issubmnd  18720  mhmima  18784  rhmimasubrng  20534  maducoeval2  22615  cramerlem3  22664  restnlly  23457  efgh  26518  hasheuni  34245  matunitlindflem1  37951  pellex  43281  mendlmod  43635  disjf1o  45639  ssfiunibd  45760  mullimc  46064  mullimcf  46071  limclner  46097  limsupresxr  46212  liminfresxr  46213  sge0lefi  46844  isomenndlem  46976  hoicvr  46994  ovncvrrp  47010