Theorem mulassd 11335

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11269

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  recex  11951  mulcand  11952  receu  11964  divmulasscom  12001  divdivdiv  12021  divmuleq  12025  conjmul  12037  modmul1  14070  moddi  14085  expadd  14250  mulbinom2  14370  binom3  14371  digit1  14384  discr1  14386  discr  14387  faclbnd  14437  faclbnd6  14446  bcm1k  14462  bcp1nk  14464  crre  15286  remullem  15300  amgm2  15542  iseraltlem2  15855  iseraltlem3  15856  binomlem  16003  climcndslem2  16024  pwdif  16042  geo2sum  16047  mertenslem1  16058  clim2prod  16062  fallrisefac  16197  binomfallfaclem2  16211  bpolydiflem  16225  bpoly4  16230  sinadd  16337  tanadd  16340  pwp1fsum  16566  bezoutlem3  16719  dvdsmulgcd  16735  qredeq  16837  pcaddlem  17071  prmpwdvds  17087  ablfacrp  20287  nmoco  25061  cph2ass  25539  cphipval2  25567  csbren  25725  minveclem2  25752  uniioombllem5  25913  itg1mulc  26030  mbfi1fseqlem5  26045  itgconst  26144  itgmulc2  26159  dvexp  26278  dvply1  26610  elqaalem3  26649  aalioulem1  26664  aaliou3lem2  26675  dvtaylp  26702  dvradcnv  26753  pserdvlem2  26760  tangtx  26839  tanregt0  26872  tanarg  26952  logcnlem4  26978  cxpmul  27021  dvcxp1  27073  dvcncxp1  27076  root1eq1  27088  heron  27171  quad2  27172  dcubic1lem  27176  dcubic1  27178  cubic2  27181  binom4  27183  dquartlem1  27184  dquartlem2  27185  dquart  27186  quart1lem  27188  quart1  27189  quartlem1  27190  efiasin  27221  asinsinlem  27224  asinsin  27225  efiatan  27245  efiatan2  27250  2efiatan  27251  atantan  27256  atanbndlem  27258  atans2  27264  atantayl  27270  log2cnv  27277  log2tlbnd  27278  ftalem1  27405  ftalem5  27409  basellem3  27415  basellem5  27417  basellem8  27420  chtub  27544  perfectlem1  27561  perfectlem2  27562  perfect  27563  bcmono  27609  bclbnd  27612  bposlem9  27624  lgsneg  27653  gausslemma2dlem6  27704  lgseisenlem1  27707  lgseisenlem2  27708  lgseisenlem3  27709  lgseisenlem4  27710  lgsquad2lem1  27716  lgsquad3  27719  2lgslem3a  27728  2lgslem3b  27729  2lgslem3c  27730  2lgslem3d  27731  2lgsoddprmlem2  27741  2sqlem3  27752  chto1ub  27808  rplogsumlem1  27816  dchrmusum2  27826  dchrvmasum2lem  27828  dchrvmasumlem2  27830  dchrvmasumiflem2  27834  dchrisum0lem1  27848  dchrisum0lem2  27850  mulog2sumlem2  27867  chpdifbndlem1  27885  selberg3lem1  27889  selberg4lem1  27892  selberg34r  27903  pntrlog2bndlem3  27911  pntrlog2bndlem5  27913  pntrlog2bndlem6  27915  pntlemh  27931  pntlemr  27934  pntlemf  27937  pntlemk  27938  pntlemo  27939  flt4lem5e  27991  flt4lem5f  27992  colinearalglem4  29492  axpasch  29524  axcontlem2  29548  axcontlem4  29550  axcontlem7  29553  axcontlem8  29554  ipasslem4  31441  minvecolem2  31482  his35  31695  leopnmid  32745  quad3d  33387  zringfrac  34132  ccfldsrarelvec  34349  constrrtll  34409  constrrtlc1  34410  constrrtcclem  34412  constrrtcc  34413  cos9thpiminplylem2  34461  oddpwdc  35032  prodfzo03  35278  itgexpif  35281  breprexplemc  35307  circlemeth  35315  hgt750lemg  35329  hgt750lemb  35331  hgt750leme  35333  subfacval2  36038  subfaclim  36039  circum  36525  faclimlem1  36600  faclimlem3  36602  faclim2  36605  unbdqndv2lem1  37467  knoppndvlem2  37471  knoppndvlem7  37476  knoppndvlem11  37480  knoppndvlem12  37481  knoppndvlem14  37483  knoppndvlem18  37487  itgmulc2nc  38699  areacirclem1  38719  areacirclem4  38722  bfplem1  38849  lcmineqlem1  43172  lcmineqlem5  43176  lcmineqlem10  43181  lcmineqlem12  43183  lcmineqlem18  43189  lcmineqlem20  43191  dvrelogpow2b  43211  aks4d1p1p7  43217  primrootscoprmpow  43242  2np3bcnp1  43287  quadfac  43348  remulcan2d  43400  remul02  43549  remul01  43551  sn-it0e0  43560  remulinvcom  43577  remullid  43578  sn-mullid  43580  remulcand  43583  rediveud  43587  redivrec2d  43604  rediv23d  43605  sn-0tie0  43608  sn-mul02  43609  mulgt0b1d  43629  mulgt0b2d  43635  mullt0b1d  43640  sn-itrere  43645  sn-retire  43646  fltnlta  43767  cu3addd  43784  3cubeslem2  43788  3cubeslem3l  43789  3cubeslem3r  43790  pellexlem6  43934  rmxluc  44036  rmyluc2  44038  rmydbl  44040  jm2.18  44088  jm2.23  44096  jm2.27c  44107  jm3.1lem2  44118  proot1ex  44291  sqrtcval  44734  sqrtcval2  44735  int-mulassocd  45270  binomcxplemnotnn0  45433  mul13d  46389  fmul01lt1lem1  46689  fmul01lt1lem2  46690  coskpi2  46969  cosknegpi  46972  dvnxpaek  47045  dvmptfprodlem  47047  dvnprodlem2  47050  itgsinexplem1  47057  stoweidlem26  47129  wallispilem5  47172  wallispi  47173  wallispi2lem1  47174  wallispi2lem2  47175  stirlinglem3  47179  stirlinglem10  47186  stirlinglem15  47191  dirkertrigeqlem1  47201  dirkertrigeqlem2  47202  dirkertrigeqlem3  47203  dirkertrigeq  47204  dirkercncflem2  47207  fourierdlem66  47275  fourierswlem  47333  fouriersw  47334  etransclem23  47360  etransclem25  47362  etransclem46  47383  hoidmvlelem2  47699  sigarls  47960  sharhght  47968  sin3t  48010  cos3t  48011  sin5tlem2  48013  sin5tlem3  48014  sin5tlem4  48015  modmkpkne  48530  fmtnorec4  48727  fmtnoprmfac2lem1  48744  fmtnoprmfac2  48745  fmtnofac2lem  48746  fmtnofac1  48748  lighneallem4a  48786  perfectALTVlem1  48912  perfectALTVlem2  48913  perfectALTV  48914  2zrngmmgm  49442  altgsumbcALT  49558  nn0sumshdiglemB  49825  affinecomb2  49908  itscnhlc0yqe  49964  itschlc0yqe  49965  itsclc0yqsollem1  49967  itsclc0yqsol  49969  itscnhlc0xyqsol  49970  itsclc0xyqsolr  49974  itsclquadb  49981  aacllem  51107  crosspdotd  51133  crossp3d  51135