Theorem mulassd 11234

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   · cmul 11112

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090

This theorem is referenced by:  recex  11843  mulcand  11844  receu  11856  divmulasscom  11893  divdivdiv  11912  divmuleq  11916  conjmul  11928  modmul1  13886  moddi  13901  expadd  14067  mulbinom2  14183  binom3  14184  digit1  14197  discr1  14199  discr  14200  faclbnd  14247  faclbnd6  14256  bcm1k  14272  bcp1nk  14274  crre  15058  remullem  15072  amgm2  15313  iseraltlem2  15626  iseraltlem3  15627  binomlem  15772  climcndslem2  15793  pwdif  15811  geo2sum  15816  mertenslem1  15827  clim2prod  15831  fallrisefac  15966  binomfallfaclem2  15981  bpolydiflem  15995  bpoly4  16000  sinadd  16104  tanadd  16107  pwp1fsum  16331  bezoutlem3  16480  dvdsmulgcd  16494  qredeq  16591  pcaddlem  16818  prmpwdvds  16834  ablfacrp  19931  nmoco  24246  cph2ass  24722  cphipval2  24750  csbren  24908  minveclem2  24935  uniioombllem5  25096  itg1mulc  25214  mbfi1fseqlem5  25229  itgconst  25328  itgmulc2  25343  dvexp  25462  dvply1  25789  elqaalem3  25826  aalioulem1  25837  aaliou3lem2  25848  dvtaylp  25874  dvradcnv  25925  pserdvlem2  25932  tangtx  26007  tanregt0  26040  tanarg  26119  logcnlem4  26145  cxpmul  26188  dvcxp1  26238  dvcncxp1  26241  root1eq1  26253  heron  26333  quad2  26334  dcubic1lem  26338  dcubic1  26340  cubic2  26343  binom4  26345  dquartlem1  26346  dquartlem2  26347  dquart  26348  quart1lem  26350  quart1  26351  quartlem1  26352  efiasin  26383  asinsinlem  26386  asinsin  26387  efiatan  26407  efiatan2  26412  2efiatan  26413  atantan  26418  atanbndlem  26420  atans2  26426  atantayl  26432  log2cnv  26439  log2tlbnd  26440  ftalem1  26567  ftalem5  26571  basellem3  26577  basellem5  26579  basellem8  26582  chtub  26705  perfectlem1  26722  perfectlem2  26723  perfect  26724  bcmono  26770  bclbnd  26773  bposlem9  26785  lgsneg  26814  gausslemma2dlem6  26865  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgseisenlem4  26871  lgsquad2lem1  26877  lgsquad3  26880  2lgslem3a  26889  2lgslem3b  26890  2lgslem3c  26891  2lgslem3d  26892  2lgsoddprmlem2  26902  2sqlem3  26913  chto1ub  26969  rplogsumlem1  26977  dchrmusum2  26987  dchrvmasum2lem  26989  dchrvmasumlem2  26991  dchrvmasumiflem2  26995  dchrisum0lem1  27009  dchrisum0lem2  27011  mulog2sumlem2  27028  chpdifbndlem1  27046  selberg3lem1  27050  selberg4lem1  27053  selberg34r  27064  pntrlog2bndlem3  27072  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntlemh  27092  pntlemr  27095  pntlemf  27098  pntlemk  27099  pntlemo  27100  colinearalglem4  28157  axpasch  28189  axcontlem2  28213  axcontlem4  28215  axcontlem7  28218  axcontlem8  28219  ipasslem4  30075  minvecolem2  30116  his35  30329  leopnmid  31379  ccfldsrarelvec  32734  oddpwdc  33342  prodfzo03  33604  itgexpif  33607  breprexplemc  33633  circlemeth  33641  hgt750lemg  33655  hgt750lemb  33657  hgt750leme  33659  subfacval2  34167  subfaclim  34168  circum  34648  faclimlem1  34702  faclimlem3  34704  faclim2  34707  unbdqndv2lem1  35374  knoppndvlem2  35378  knoppndvlem7  35383  knoppndvlem11  35387  knoppndvlem12  35388  knoppndvlem14  35390  knoppndvlem18  35394  itgmulc2nc  36545  areacirclem1  36565  areacirclem4  36568  bfplem1  36679  lcmineqlem1  40883  lcmineqlem5  40887  lcmineqlem10  40892  lcmineqlem12  40894  lcmineqlem18  40900  lcmineqlem20  40902  dvrelogpow2b  40922  aks4d1p1p7  40928  2np3bcnp1  40949  remulcan2d  41175  remul02  41275  remul01  41277  sn-it0e0  41285  remulinvcom  41302  remullid  41303  sn-mullid  41305  remulcand  41308  sn-0tie0  41309  sn-mul02  41310  mulgt0b2d  41330  itrere  41336  retire  41337  flt4lem5e  41395  flt4lem5f  41396  fltnlta  41402  cu3addd  41404  3cubeslem2  41409  3cubeslem3l  41410  3cubeslem3r  41411  pellexlem6  41558  rmxluc  41661  rmyluc2  41663  rmydbl  41665  jm2.18  41713  jm2.23  41721  jm2.27c  41732  jm3.1lem2  41743  proot1ex  41929  sqrtcval  42378  sqrtcval2  42379  int-mulassocd  42915  binomcxplemnotnn0  43101  mul13d  43976  fmul01lt1lem1  44287  fmul01lt1lem2  44288  coskpi2  44569  cosknegpi  44572  dvnxpaek  44645  dvmptfprodlem  44647  dvnprodlem2  44650  itgsinexplem1  44657  stoweidlem26  44729  wallispilem5  44772  wallispi  44773  wallispi2lem1  44774  wallispi2lem2  44775  stirlinglem3  44779  stirlinglem10  44786  stirlinglem15  44791  dirkertrigeqlem1  44801  dirkertrigeqlem2  44802  dirkertrigeqlem3  44803  dirkertrigeq  44804  dirkercncflem2  44807  fourierdlem66  44875  fourierswlem  44933  fouriersw  44934  etransclem23  44960  etransclem25  44962  etransclem46  44983  hoidmvlelem2  45299  sigarls  45560  sharhght  45568  fmtnorec4  46204  fmtnoprmfac2lem1  46221  fmtnoprmfac2  46222  fmtnofac2lem  46223  fmtnofac1  46225  lighneallem4a  46263  perfectALTVlem1  46376  perfectALTVlem2  46377  perfectALTV  46378  2zrngmmgm  46798  altgsumbcALT  46983  nn0sumshdiglemB  47260  affinecomb2  47343  itscnhlc0yqe  47399  itschlc0yqe  47400  itsclc0yqsollem1  47402  itsclc0yqsol  47404  itscnhlc0xyqsol  47405  itsclc0xyqsolr  47409  itsclquadb  47416  aacllem  47802