Theorem 3adant1l 1358

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 1285	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	adantll 750	. 2 ⊢ (((𝜏 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	3	3impb 1279	1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3adant2l  1360  3adant3l  1362  cfsmolem  9130  axdc3lem4  9313  issubmnd  17365  maducoeval2  20494  cramerlem3  20543  restnlly  21333  efgh  24332  funvtxdm2valOLD  25940  funiedgdm2valOLD  25941  hasheuni  30275  matunitlindflem1  33535  pellex  37716  mendlmod  38080  disjf1o  39692  ssfiunibd  39837  mullimc  40166  mullimcf  40173  limclner  40201  limsupresxr  40316  liminfresxr  40317  sge0lefi  40933  isomenndlem  41065  hoicvr  41083  ovncvrrp  41099