Theorem 3adantl1 1166

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

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

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 1089

This theorem is referenced by:  3ad2antl2  1186  3ad2antl3  1187  funcnvqp  6612  onfununi  8343  omord2  8569  en2eqpr  10004  divmuldiv  11916  ioojoin  13462  expnlbnd  14198  swrdlend  14605  2cshw  14765  lcmledvds  16538  pospropd  18282  marrepcl  22073  gsummatr01lem3  22166  upxp  23134  rnelfmlem  23463  brbtwn2  28201  wlkonprop  28953  trlsonprop  29003  pthsonprop  29039  spthonprop  29040  spthonepeq  29047  fh2  30910  homulass  31093  hoadddi  31094  hoadddir  31095  metf1o  36709  rngohomco  36928  rngoisoco  36936  op01dm  38139  paddss12  38776  wessf1ornlem  43963  elaa2  45029  smflimlem2  45567