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  6634  onfununi  8387  omord2  8613  en2eqpr  10125  divmuldiv  12057  ioojoin  13654  expnlbnd  14418  swrdlend  14845  2cshw  15006  lcmledvds  16818  pospropd  18549  marrepcl  22934  gsummatr01lem3  23027  upxp  23997  rnelfmlem  24326  brbtwn2  29540  wlkonprop  30294  trlsonprop  30347  pthsonprop  30387  spthonprop  30388  spthonepeq  30395  fh2  32278  homulass  32461  hoadddi  32462  hoadddir  32463  ltnmul  37180  metf1o  38955  rngohomco  39174  rngoisoco  39182  op01dm  40506  paddss12  41142  wessf1ornlem  46473  elaa2  47517  smflimlem2  48055