Theorem 3adant1l 1310

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
3adant1l.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant1l	⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant1l

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1258	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	adantll 746	. 2 ⊢ (((𝜏 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	3	3impb 1252	1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3adant2l  1312  3adant3l  1314  cfsmolem  8975  axdc3lem4  9158  issubmnd  17141  maducoeval2  20265  cramerlem3  20314  restnlly  21095  efgh  24091  funvtxdm2val  25688  funiedgdm2val  25689  hasheuni  29474  matunitlindflem1  32575  pellex  36417  mendlmod  36782  disjf1o  38373  ssfiunibd  38464  mullimc  38683  mullimcf  38690  limclner  38718  sge0lefi  39291  isomenndlem  39420  hoicvr  39438  ovncvrrp  39454