Theorem 3adantl1 1162

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3ad2antl2  1182  3ad2antl3  1183  funcnvqp  6418  onfununi  7978  omord2  8193  en2eqpr  9433  divmuldiv  11340  ioojoin  12870  expnlbnd  13595  swrdlend  14015  2cshw  14175  lcmledvds  15943  pospropd  17744  marrepcl  21173  gsummatr01lem3  21266  upxp  22231  rnelfmlem  22560  brbtwn2  26691  wlkonprop  27440  trlsonprop  27489  pthsonprop  27525  spthonprop  27526  spthonepeq  27533  fh2  29396  homulass  29579  hoadddi  29580  hoadddir  29581  metf1o  35045  rngohomco  35267  rngoisoco  35275  op01dm  36334  paddss12  36970  wessf1ornlem  41465  elaa2  42539  smflimlem2  43068