Theorem 3adantl1 1168

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  3ad2antl2  1194  3ad2antl3  1195  funcnvqp  6198  onfununi  7721  omord2  7931  en2eqpr  9163  divmuldiv  11075  ioojoin  12620  expnlbnd  13313  swrdlend  13748  lcmledvds  15718  pospropd  17520  marrepcl  20775  gsummatr01lem3  20869  upxp  21835  rnelfmlem  22164  brbtwn2  26254  spthonepeq  27104  fh2  29050  homulass  29233  hoadddi  29234  hoadddir  29235  metf1o  34175  rngohomco  34397  rngoisoco  34405  op01dm  35337  paddss12  35973  wessf1ornlem  40294  elaa2  41378  smflimlem2  41907