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  6604  onfununi  8330  omord2  8554  en2eqpr  10003  divmuldiv  11926  ioojoin  13522  expnlbnd  14283  swrdlend  14709  2cshw  14870  lcmledvds  16675  pospropd  18399  marrepcl  22751  gsummatr01lem3  22844  upxp  23811  rnelfmlem  24140  brbtwn2  29286  wlkonprop  30040  trlsonprop  30093  pthsonprop  30133  spthonprop  30134  spthonepeq  30141  fh2  32018  homulass  32201  hoadddi  32202  hoadddir  32203  ltnmul  36721  metf1o  38439  rngohomco  38658  rngoisoco  38666  op01dm  39990  paddss12  40626  wessf1ornlem  45936  elaa2  46981  smflimlem2  47519