Theorem 3adantl1 1167

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3ad2antl2  1187  3ad2antl3  1188  funcnvqp  6556  onfununi  8273  omord2  8494  en2eqpr  9917  divmuldiv  11841  ioojoin  13399  expnlbnd  14156  swrdlend  14577  2cshw  14736  lcmledvds  16526  pospropd  18248  marrepcl  22508  gsummatr01lem3  22601  upxp  23567  rnelfmlem  23896  brbtwn2  28978  wlkonprop  29730  trlsonprop  29779  pthsonprop  29817  spthonprop  29818  spthonepeq  29825  fh2  31694  homulass  31877  hoadddi  31878  hoadddir  31879  metf1o  37956  rngohomco  38175  rngoisoco  38183  op01dm  39443  paddss12  40079  wessf1ornlem  45429  elaa2  46478  smflimlem2  47016