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  6602  onfununi  8342  omord2  8568  en2eqpr  10079  divmuldiv  12010  ioojoin  13607  expnlbnd  14370  swrdlend  14796  2cshw  14957  lcmledvds  16767  pospropd  18492  marrepcl  22872  gsummatr01lem3  22965  upxp  23935  rnelfmlem  24264  brbtwn2  29476  wlkonprop  30230  trlsonprop  30283  pthsonprop  30323  spthonprop  30324  spthonepeq  30331  fh2  32214  homulass  32397  hoadddi  32398  hoadddir  32399  ltnmul  36945  metf1o  38669  rngohomco  38888  rngoisoco  38896  op01dm  40220  paddss12  40856  wessf1ornlem  46169  elaa2  47213  smflimlem2  47751