Theorem mulassd 10664

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 10625	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1367	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   · cmul 10542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10603

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  recex  11272  mulcand  11273  receu  11285  divmulasscom  11322  divdivdiv  11341  divmuleq  11345  conjmul  11357  modmul1  13293  moddi  13308  expadd  13472  mulbinom2  13585  binom3  13586  digit1  13599  discr1  13601  discr  13602  faclbnd  13651  faclbnd6  13660  bcm1k  13676  bcp1nk  13678  crre  14473  remullem  14487  amgm2  14729  iseraltlem2  15039  iseraltlem3  15040  binomlem  15184  climcndslem2  15205  pwdif  15223  geo2sum  15229  mertenslem1  15240  clim2prod  15244  fallrisefac  15379  binomfallfaclem2  15394  bpolydiflem  15408  bpoly4  15413  sinadd  15517  tanadd  15520  pwp1fsum  15742  bezoutlem3  15889  dvdsmulgcd  15905  qredeq  16001  pcaddlem  16224  prmpwdvds  16240  ablfacrp  19188  nmoco  23346  cph2ass  23817  cphipval2  23844  csbren  24002  minveclem2  24029  uniioombllem5  24188  itg1mulc  24305  mbfi1fseqlem5  24320  itgconst  24419  itgmulc2  24434  dvexp  24550  dvply1  24873  elqaalem3  24910  aalioulem1  24921  aaliou3lem2  24932  dvtaylp  24958  dvradcnv  25009  pserdvlem2  25016  tangtx  25091  tanregt0  25123  tanarg  25202  logcnlem4  25228  cxpmul  25271  dvcxp1  25321  dvcncxp1  25324  root1eq1  25336  heron  25416  quad2  25417  dcubic1lem  25421  dcubic1  25423  cubic2  25426  binom4  25428  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1lem  25433  quart1  25434  quartlem1  25435  efiasin  25466  asinsinlem  25469  asinsin  25470  efiatan  25490  efiatan2  25495  2efiatan  25496  atantan  25501  atanbndlem  25503  atans2  25509  atantayl  25515  log2cnv  25522  log2tlbnd  25523  ftalem1  25650  ftalem5  25654  basellem3  25660  basellem5  25662  basellem8  25665  chtub  25788  perfectlem1  25805  perfectlem2  25806  perfect  25807  bcmono  25853  bclbnd  25856  bposlem9  25868  lgsneg  25897  gausslemma2dlem6  25948  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgsquad2lem1  25960  lgsquad3  25963  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgsoddprmlem2  25985  2sqlem3  25996  chto1ub  26052  rplogsumlem1  26060  dchrmusum2  26070  dchrvmasum2lem  26072  dchrvmasumlem2  26074  dchrvmasumiflem2  26078  dchrisum0lem1  26092  dchrisum0lem2  26094  mulog2sumlem2  26111  chpdifbndlem1  26129  selberg3lem1  26133  selberg4lem1  26136  selberg34r  26147  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntlemh  26175  pntlemr  26178  pntlemf  26181  pntlemk  26182  pntlemo  26183  colinearalglem4  26695  axpasch  26727  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  ipasslem4  28611  minvecolem2  28652  his35  28865  leopnmid  29915  ccfldsrarelvec  31056  oddpwdc  31612  prodfzo03  31874  itgexpif  31877  breprexplemc  31903  circlemeth  31911  hgt750lemg  31925  hgt750lemb  31927  hgt750leme  31929  subfacval2  32434  subfaclim  32435  circum  32917  faclimlem1  32975  faclimlem3  32977  faclim2  32980  unbdqndv2lem1  33848  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem11  33861  knoppndvlem12  33862  knoppndvlem14  33864  knoppndvlem18  33868  itgmulc2nc  34975  areacirclem1  34997  areacirclem4  35000  bfplem1  35115  remulcan2d  39205  remul02  39284  remul01  39286  remulinvcom  39297  remulid2  39298  remulcand  39299  fltnlta  39324  cu3addd  39326  3cubeslem2  39331  3cubeslem3l  39332  3cubeslem3r  39333  pellexlem6  39480  rmxluc  39582  rmyluc2  39584  rmydbl  39586  jm2.18  39634  jm2.23  39642  jm2.27c  39653  jm3.1lem2  39664  proot1ex  39850  int-mulassocd  40579  binomcxplemnotnn0  40737  mul13d  41594  fmul01lt1lem1  41914  fmul01lt1lem2  41915  coskpi2  42196  cosknegpi  42199  dvnxpaek  42276  dvmptfprodlem  42278  dvnprodlem2  42281  itgsinexplem1  42288  stoweidlem26  42360  wallispilem5  42403  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem3  42410  stirlinglem10  42417  stirlinglem15  42422  dirkertrigeqlem1  42432  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkercncflem2  42438  fourierdlem66  42506  fourierswlem  42564  fouriersw  42565  etransclem23  42591  etransclem25  42593  etransclem46  42614  hoidmvlelem2  42927  sigarls  43163  sharhght  43171  fmtnorec4  43760  fmtnoprmfac2lem1  43777  fmtnoprmfac2  43778  fmtnofac2lem  43779  fmtnofac1  43781  lighneallem4a  43822  perfectALTVlem1  43935  perfectALTVlem2  43936  perfectALTV  43937  2zrngmmgm  44266  altgsumbcALT  44450  nn0sumshdiglemB  44729  affinecomb2  44739  itscnhlc0yqe  44795  itschlc0yqe  44796  itsclc0yqsollem1  44798  itsclc0yqsol  44800  itscnhlc0xyqsol  44801  itsclc0xyqsolr  44805  itsclquadb  44812  aacllem  44951