Theorem mulassd 8349

Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
mulassd	⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulassd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mulass 8310	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1278	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   · cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-mulass 8282

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ltmul1  8921  recexap  8982  mulap0  8983  mulcanapd  8990  receuap  9000  divmulasscomap  9027  divdivdivap  9044  divmuleqap  9048  conjmulap  9060  apmul1  9119  qapne  10041  modqmul1  10816  modqdi  10831  expadd  11020  mulbinom2  11095  binom3  11096  faclbnd  11181  faclbnd6  11184  bcm1k  11200  bcp1nk  11202  bcval5  11203  crre  11624  remullem  11638  sq01  11662  resqrexlemcalc1  11782  resqrexlemnm  11786  amgm2  11886  binomlem  12252  geo2sum  12283  mertenslemi1  12304  clim2prod  12308  sinadd  12505  tanaddap  12508  dvdsmulcr  12590  dvdsmulgcd  12804  qredeq  12876  2sqpwodd  12956  pcaddlem  13120  prmpwdvds  13136  dvexp  15814  dvply1  15868  tangtx  15942  logfac  16001  cxpmul  16020  binom4  16087  log2tlbndlog2  16088  perfectlem1  16119  perfectlem2  16120  perfect  16121  bcmono  16124  bclbnd  16127  lgsneg  16155  gausslemma2dlem6  16198  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem3  16203  lgseisenlem4  16204  lgsquad2lem1  16212  lgsquad3  16215  2lgslem3a  16224  2lgslem3b  16225  2lgslem3c  16226  2lgslem3d  16227  2lgsoddprmlem2  16237  2sqlem3  16248