Theorem 3adantl1 1165

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3ad2antl2  1185  3ad2antl3  1186  funcnvqp  6549  onfununi  8243  omord2  8470  en2eqpr  9865  divmuldiv  11777  ioojoin  13317  expnlbnd  14050  swrdlend  14465  2cshw  14625  lcmledvds  16402  pospropd  18143  marrepcl  21820  gsummatr01lem3  21913  upxp  22881  rnelfmlem  23210  brbtwn2  27563  wlkonprop  28315  trlsonprop  28365  pthsonprop  28401  spthonprop  28402  spthonepeq  28409  fh2  30270  homulass  30453  hoadddi  30454  hoadddir  30455  metf1o  36069  rngohomco  36288  rngoisoco  36296  op01dm  37501  paddss12  38138  wessf1ornlem  43101  elaa2  44163  smflimlem2  44699