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  8340  omord2  8566  en2eqpr  10001  divmuldiv  11913  ioojoin  13459  expnlbnd  14195  swrdlend  14602  2cshw  14762  lcmledvds  16535  pospropd  18279  marrepcl  22065  gsummatr01lem3  22158  upxp  23126  rnelfmlem  23455  brbtwn2  28160  wlkonprop  28912  trlsonprop  28962  pthsonprop  28998  spthonprop  28999  spthonepeq  29006  fh2  30867  homulass  31050  hoadddi  31051  hoadddir  31052  metf1o  36618  rngohomco  36837  rngoisoco  36845  op01dm  38048  paddss12  38685  wessf1ornlem  43872  elaa2  44940  smflimlem2  45478