Theorem 3adantl1 1183

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 1166	. 2 ⊢ ((𝜏 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 591	1 ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3ad2antl2  1203  3ad2antl3  1204  funcnvqp  6598  onfununi  8324  omord2  8548  en2eqpr  9987  divmuldiv  11911  ioojoin  13506  expnlbnd  14265  swrdlend  14687  2cshw  14846  lcmledvds  16653  pospropd  18377  marrepcl  22686  gsummatr01lem3  22779  upxp  23745  rnelfmlem  24074  brbtwn2  29192  wlkonprop  29943  trlsonprop  29992  pthsonprop  30030  spthonprop  30031  spthonepeq  30038  fh2  31908  homulass  32091  hoadddi  32092  hoadddir  32093  metf1o  38289  rngohomco  38508  rngoisoco  38516  op01dm  39842  paddss12  40478  wessf1ornlem  45790  elaa2  46835  smflimlem2  47373