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  10192  axdc3lem4  10375  issubmnd  18729  mhmima  18793  rhmimasubrng  20543  maducoeval2  22605  cramerlem3  22654  restnlly  23447  efgh  26505  hasheuni  34229  matunitlindflem1  37937  pellex  43263  mendlmod  43617  disjf1o  45621  ssfiunibd  45742  mullimc  46046  mullimcf  46053  limclner  46079  limsupresxr  46194  liminfresxr  46195  sge0lefi  46826  isomenndlem  46958  hoicvr  46976  ovncvrrp  46992