Theorem mulassd 11235

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2150  (class class class)co 7414  ℂcc 11101   · cmul 11108

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  recex  11849  mulcand  11850  receu  11862  divmulasscom  11899  divdivdiv  11919  divmuleq  11923  conjmul  11935  modmul1  13963  moddi  13978  expadd  14143  mulbinom2  14262  binom3  14263  digit1  14276  discr1  14278  discr  14279  faclbnd  14329  faclbnd6  14338  bcm1k  14354  bcp1nk  14356  crre  15168  remullem  15182  amgm2  15424  iseraltlem2  15737  iseraltlem3  15738  binomlem  15886  climcndslem2  15907  pwdif  15925  geo2sum  15930  mertenslem1  15941  clim2prod  15945  fallrisefac  16082  binomfallfaclem2  16097  bpolydiflem  16111  bpoly4  16116  sinadd  16223  tanadd  16226  pwp1fsum  16452  bezoutlem3  16602  dvdsmulgcd  16617  qredeq  16718  pcaddlem  16951  prmpwdvds  16967  ablfacrp  20141  nmoco  24877  cph2ass  25355  cphipval2  25383  csbren  25541  minveclem2  25568  uniioombllem5  25729  itg1mulc  25846  mbfi1fseqlem5  25861  itgconst  25961  itgmulc2  25976  dvexp  26095  dvply1  26428  elqaalem3  26465  aalioulem1  26476  aaliou3lem2  26487  dvtaylp  26513  dvradcnv  26564  pserdvlem2  26571  tangtx  26650  tanregt0  26684  tanarg  26764  logcnlem4  26790  cxpmul  26833  dvcxp1  26885  dvcncxp1  26888  root1eq1  26900  heron  26983  quad2  26984  dcubic1lem  26988  dcubic1  26990  cubic2  26993  binom4  26995  dquartlem1  26996  dquartlem2  26997  dquart  26998  quart1lem  27000  quart1  27001  quartlem1  27002  efiasin  27033  asinsinlem  27036  asinsin  27037  efiatan  27057  efiatan2  27062  2efiatan  27063  atantan  27068  atanbndlem  27070  atans2  27076  atantayl  27082  log2cnv  27089  log2tlbnd  27090  ftalem1  27217  ftalem5  27221  basellem3  27227  basellem5  27229  basellem8  27232  chtub  27356  perfectlem1  27373  perfectlem2  27374  perfect  27375  bcmono  27421  bclbnd  27424  bposlem9  27436  lgsneg  27465  gausslemma2dlem6  27516  lgseisenlem1  27519  lgseisenlem2  27520  lgseisenlem3  27521  lgseisenlem4  27522  lgsquad2lem1  27528  lgsquad3  27531  2lgslem3a  27540  2lgslem3b  27541  2lgslem3c  27542  2lgslem3d  27543  2lgsoddprmlem2  27553  2sqlem3  27564  chto1ub  27620  rplogsumlem1  27628  dchrmusum2  27638  dchrvmasum2lem  27640  dchrvmasumlem2  27642  dchrvmasumiflem2  27646  dchrisum0lem1  27660  dchrisum0lem2  27662  mulog2sumlem2  27679  chpdifbndlem1  27697  selberg3lem1  27701  selberg4lem1  27704  selberg34r  27715  pntrlog2bndlem3  27723  pntrlog2bndlem5  27725  pntrlog2bndlem6  27727  pntlemh  27743  pntlemr  27746  pntlemf  27749  pntlemk  27750  pntlemo  27751  colinearalglem4  29229  axpasch  29261  axcontlem2  29285  axcontlem4  29287  axcontlem7  29290  axcontlem8  29291  ipasslem4  31156  minvecolem2  31197  his35  31410  leopnmid  32460  quad3d  33064  zringfrac  33814  ccfldsrarelvec  34031  constrrtll  34091  constrrtlc1  34092  constrrtcclem  34094  constrrtcc  34095  cos9thpiminplylem2  34143  oddpwdc  34714  prodfzo03  34960  itgexpif  34963  breprexplemc  34989  circlemeth  34997  hgt750lemg  35011  hgt750lemb  35013  hgt750leme  35015  subfacval2  35637  subfaclim  35638  circum  36124  faclimlem1  36193  faclimlem3  36195  faclim2  36198  unbdqndv2lem1  37046  knoppndvlem2  37050  knoppndvlem7  37055  knoppndvlem11  37059  knoppndvlem12  37060  knoppndvlem14  37062  knoppndvlem18  37066  itgmulc2nc  38287  areacirclem1  38307  areacirclem4  38310  bfplem1  38421  lcmineqlem1  42746  lcmineqlem5  42750  lcmineqlem10  42755  lcmineqlem12  42757  lcmineqlem18  42763  lcmineqlem20  42765  dvrelogpow2b  42785  aks4d1p1p7  42791  primrootscoprmpow  42816  2np3bcnp1  42861  quadfac  42922  remulcan2d  42974  remul02  43116  remul01  43118  sn-it0e0  43127  remulinvcom  43144  remullid  43145  sn-mullid  43147  remulcand  43150  rediveud  43154  redivrec2d  43171  rediv23d  43172  sn-0tie0  43175  sn-mul02  43176  mulgt0b1d  43196  mulgt0b2d  43202  mullt0b1d  43207  sn-itrere  43212  sn-retire  43213  flt4lem5e  43340  flt4lem5f  43341  fltnlta  43347  cu3addd  43364  3cubeslem2  43368  3cubeslem3l  43369  3cubeslem3r  43370  pellexlem6  43513  rmxluc  43615  rmyluc2  43617  rmydbl  43619  jm2.18  43667  jm2.23  43675  jm2.27c  43686  jm3.1lem2  43697  proot1ex  43875  sqrtcval  44319  sqrtcval2  44320  int-mulassocd  44855  binomcxplemnotnn0  45018  mul13d  45951  fmul01lt1lem1  46252  fmul01lt1lem2  46253  coskpi2  46532  cosknegpi  46535  dvnxpaek  46608  dvmptfprodlem  46610  dvnprodlem2  46613  itgsinexplem1  46620  stoweidlem26  46692  wallispilem5  46735  wallispi  46736  wallispi2lem1  46737  wallispi2lem2  46738  stirlinglem3  46742  stirlinglem10  46749  stirlinglem15  46754  dirkertrigeqlem1  46764  dirkertrigeqlem2  46765  dirkertrigeqlem3  46766  dirkertrigeq  46767  dirkercncflem2  46770  fourierdlem66  46838  fourierswlem  46896  fouriersw  46897  etransclem23  46923  etransclem25  46925  etransclem46  46946  hoidmvlelem2  47262  sigarls  47523  sharhght  47531  sin3t  47557  cos3t  47558  sin5tlem2  47560  sin5tlem3  47561  sin5tlem4  47562  modmkpkne  48053  fmtnorec4  48250  fmtnoprmfac2lem1  48267  fmtnoprmfac2  48268  fmtnofac2lem  48269  fmtnofac1  48271  lighneallem4a  48309  perfectALTVlem1  48435  perfectALTVlem2  48436  perfectALTV  48437  2zrngmmgm  48966  altgsumbcALT  49082  nn0sumshdiglemB  49349  affinecomb2  49432  itscnhlc0yqe  49488  itschlc0yqe  49489  itsclc0yqsollem1  49491  itsclc0yqsol  49493  itscnhlc0xyqsol  49494  itsclc0xyqsolr  49498  itsclquadb  49505  aacllem  50550