Theorem 3adantl1 1185

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adantl1

Step	Hyp	Ref	Expression
1		3simpc 1168	. 2 ⊢ ((𝜏 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 592	1 ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2antl2  1205  3ad2antl3  1206  funcnvqp  6597  onfununi  8330  omord2  8554  en2eqpr  10010  divmuldiv  11939  ioojoin  13536  expnlbnd  14297  swrdlend  14723  2cshw  14884  lcmledvds  16689  pospropd  18413  marrepcl  22786  gsummatr01lem3  22879  upxp  23849  rnelfmlem  24178  brbtwn2  29362  wlkonprop  30116  trlsonprop  30169  pthsonprop  30209  spthonprop  30210  spthonepeq  30217  fh2  32100  homulass  32283  hoadddi  32284  hoadddir  32285  ltnmul  36796  metf1o  38505  rngohomco  38724  rngoisoco  38732  op01dm  40056  paddss12  40692  wessf1ornlem  46017  elaa2  47062  smflimlem2  47600