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  10183  axdc3lem4  10366  issubmnd  18653  mhmima  18717  rhmimasubrng  20469  maducoeval2  22543  cramerlem3  22592  restnlly  23385  efgh  26466  hasheuni  34051  matunitlindflem1  37595  pellex  42808  mendlmod  43162  disjf1o  45169  ssfiunibd  45291  mullimc  45598  mullimcf  45605  limclner  45633  limsupresxr  45748  liminfresxr  45749  sge0lefi  46380  isomenndlem  46512  hoicvr  46530  ovncvrrp  46546