Theorem 3adant1l 1183

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ad5ant245  1369  cfsmolem  10190  axdc3lem4  10373  issubmnd  18727  mhmima  18791  rhmimasubrng  20545  maducoeval2  22630  cramerlem3  22679  restnlly  23472  efgh  26530  hasheuni  34276  matunitlindflem1  37990  pellex  43287  mendlmod  43641  disjf1o  45645  ssfiunibd  45764  mullimc  46068  mullimcf  46075  limclner  46101  limsupresxr  46216  liminfresxr  46217  sge0lefi  46848  isomenndlem  46980  hoicvr  46998  ovncvrrp  47014