Theorem 3adantl1 1168

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3ad2antl2  1188  3ad2antl3  1189  funcnvqp  6562  onfununi  8281  omord2  8502  en2eqpr  9929  divmuldiv  11855  ioojoin  13436  expnlbnd  14195  swrdlend  14616  2cshw  14775  lcmledvds  16568  pospropd  18291  marrepcl  22529  gsummatr01lem3  22622  upxp  23588  rnelfmlem  23917  brbtwn2  28974  wlkonprop  29725  trlsonprop  29774  pthsonprop  29812  spthonprop  29813  spthonepeq  29820  fh2  31690  homulass  31873  hoadddi  31874  hoadddir  31875  metf1o  38076  rngohomco  38295  rngoisoco  38303  op01dm  39629  paddss12  40265  wessf1ornlem  45615  elaa2  46662  smflimlem2  47200