Theorem 3adantl1 1163

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3ad2antl2  1183  3ad2antl3  1184  funcnvqp  6388  onfununi  7961  omord2  8176  en2eqpr  9418  divmuldiv  11329  ioojoin  12861  expnlbnd  13590  swrdlend  14006  2cshw  14166  lcmledvds  15933  pospropd  17736  marrepcl  21169  gsummatr01lem3  21262  upxp  22228  rnelfmlem  22557  brbtwn2  26699  wlkonprop  27448  trlsonprop  27497  pthsonprop  27533  spthonprop  27534  spthonepeq  27541  fh2  29402  homulass  29585  hoadddi  29586  hoadddir  29587  metf1o  35193  rngohomco  35412  rngoisoco  35420  op01dm  36479  paddss12  37115  wessf1ornlem  41811  elaa2  42876  smflimlem2  43405