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  6605  onfununi  8353  omord2  8579  en2eqpr  10090  divmuldiv  12021  ioojoin  13618  expnlbnd  14381  swrdlend  14808  2cshw  14969  lcmledvds  16780  pospropd  18505  marrepcl  22885  gsummatr01lem3  22978  upxp  23948  rnelfmlem  24277  brbtwn2  29489  wlkonprop  30243  trlsonprop  30296  pthsonprop  30336  spthonprop  30337  spthonepeq  30344  fh2  32227  homulass  32410  hoadddi  32411  hoadddir  32412  ltnmul  37058  metf1o  38783  rngohomco  39002  rngoisoco  39010  op01dm  40334  paddss12  40970  wessf1ornlem  46294  elaa2  47338  smflimlem2  47876