Theorem 3adantl1 1167

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 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3ad2antl2  1187  3ad2antl3  1188  funcnvqp  6600  onfununi  8355  omord2  8579  en2eqpr  10021  divmuldiv  11941  ioojoin  13500  expnlbnd  14251  swrdlend  14671  2cshw  14831  lcmledvds  16618  pospropd  18337  marrepcl  22502  gsummatr01lem3  22595  upxp  23561  rnelfmlem  23890  brbtwn2  28884  wlkonprop  29638  trlsonprop  29688  pthsonprop  29726  spthonprop  29727  spthonepeq  29734  fh2  31600  homulass  31783  hoadddi  31784  hoadddir  31785  metf1o  37779  rngohomco  37998  rngoisoco  38006  op01dm  39201  paddss12  39838  wessf1ornlem  45209  elaa2  46263  smflimlem2  46801