Theorem mulassd 11362

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7446  ℂcc 11228   · cmul 11235

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

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

This theorem is used by:  recex  11978  mulcand  11979  receu  11991  divmulasscom  12028  divdivdiv  12048  divmuleq  12052  conjmul  12064  modmul1  14097  moddi  14112  expadd  14277  mulbinom2  14397  binom3  14398  digit1  14411  discr1  14413  discr  14414  faclbnd  14464  faclbnd6  14473  bcm1k  14489  bcp1nk  14491  crre  15313  remullem  15327  amgm2  15569  iseraltlem2  15882  iseraltlem3  15883  binomlem  16030  climcndslem2  16051  pwdif  16069  geo2sum  16074  mertenslem1  16085  clim2prod  16089  fallrisefac  16224  binomfallfaclem2  16238  bpolydiflem  16252  bpoly4  16257  sinadd  16364  tanadd  16367  pwp1fsum  16593  bezoutlem3  16746  dvdsmulgcd  16762  qredeq  16864  pcaddlem  17098  prmpwdvds  17114  ablfacrp  20315  nmoco  25089  cph2ass  25567  cphipval2  25595  csbren  25753  minveclem2  25780  uniioombllem5  25941  itg1mulc  26058  mbfi1fseqlem5  26073  itgconst  26172  itgmulc2  26187  dvexp  26306  dvply1  26638  elqaalem3  26677  aalioulem1  26692  aaliou3lem2  26703  dvtaylp  26730  dvradcnv  26781  pserdvlem2  26788  tangtx  26867  tanregt0  26900  tanarg  26980  logcnlem4  27006  cxpmul  27049  dvcxp1  27101  dvcncxp1  27104  root1eq1  27116  heron  27199  quad2  27200  dcubic1lem  27204  dcubic1  27206  cubic2  27209  binom4  27211  dquartlem1  27212  dquartlem2  27213  dquart  27214  quart1lem  27216  quart1  27217  quartlem1  27218  efiasin  27249  asinsinlem  27252  asinsin  27253  efiatan  27273  efiatan2  27278  2efiatan  27279  atantan  27284  atanbndlem  27286  atans2  27292  atantayl  27298  log2cnv  27305  log2tlbnd  27306  ftalem1  27433  ftalem5  27437  basellem3  27443  basellem5  27445  basellem8  27448  chtub  27572  perfectlem1  27589  perfectlem2  27590  perfect  27591  bcmono  27637  bclbnd  27640  bposlem9  27652  lgsneg  27681  gausslemma2dlem6  27732  lgseisenlem1  27735  lgseisenlem2  27736  lgseisenlem3  27737  lgseisenlem4  27738  lgsquad2lem1  27744  lgsquad3  27747  2lgslem3a  27756  2lgslem3b  27757  2lgslem3c  27758  2lgslem3d  27759  2lgsoddprmlem2  27769  2sqlem3  27780  chto1ub  27836  rplogsumlem1  27844  dchrmusum2  27854  dchrvmasum2lem  27856  dchrvmasumlem2  27858  dchrvmasumiflem2  27862  dchrisum0lem1  27876  dchrisum0lem2  27878  mulog2sumlem2  27895  chpdifbndlem1  27913  selberg3lem1  27917  selberg4lem1  27920  selberg34r  27931  pntrlog2bndlem3  27939  pntrlog2bndlem5  27941  pntrlog2bndlem6  27943  pntlemh  27959  pntlemr  27962  pntlemf  27965  pntlemk  27966  pntlemo  27967  flt4lem5e  28019  flt4lem5f  28020  colinearalglem4  29520  axpasch  29552  axcontlem2  29576  axcontlem4  29578  axcontlem7  29581  axcontlem8  29582  ipasslem4  31469  minvecolem2  31510  his35  31723  leopnmid  32773  quad3d  33414  zringfrac  34169  ccfldsrarelvec  34386  constrrtll  34446  constrrtlc1  34447  constrrtcclem  34449  constrrtcc  34450  cos9thpiminplylem2  34498  oddpwdc  35069  prodfzo03  35315  itgexpif  35318  breprexplemc  35344  circlemeth  35352  hgt750lemg  35366  hgt750lemb  35368  hgt750leme  35370  subfacval2  36132  subfaclim  36133  circum  36619  faclimlem1  36699  faclimlem3  36701  faclim2  36704  unbdqndv2lem1  37566  knoppndvlem2  37570  knoppndvlem7  37575  knoppndvlem11  37579  knoppndvlem12  37580  knoppndvlem14  37582  knoppndvlem18  37586  itgmulc2nc  38811  areacirclem1  38831  areacirclem4  38834  bfplem1  38959  lcmineqlem1  43282  lcmineqlem5  43286  lcmineqlem10  43291  lcmineqlem12  43293  lcmineqlem18  43299  lcmineqlem20  43301  dvrelogpow2b  43321  aks4d1p1p7  43327  primrootscoprmpow  43352  2np3bcnp1  43397  quadfac  43458  remulcan2d  43511  remul02  43660  remul01  43662  sn-it0e0  43671  remulinvcom  43688  remullid  43689  sn-mullid  43691  remulcand  43694  rediveud  43698  redivrec2d  43715  rediv23d  43716  sn-0tie0  43719  sn-mul02  43720  mulgt0b1d  43740  mulgt0b2d  43746  mullt0b1d  43751  sn-itrere  43756  sn-retire  43757  fltnlta  43878  cu3addd  43895  3cubeslem2  43899  3cubeslem3l  43900  3cubeslem3r  43901  pellexlem6  44045  rmxluc  44147  rmyluc2  44149  rmydbl  44151  jm2.18  44199  jm2.23  44207  jm2.27c  44218  jm3.1lem2  44229  proot1ex  44401  sqrtcval  44844  sqrtcval2  44845  int-mulassocd  45380  binomcxplemnotnn0  45543  mul13d  46511  fmul01lt1lem1  46811  fmul01lt1lem2  46812  coskpi2  47091  cosknegpi  47094  dvnxpaek  47167  dvmptfprodlem  47169  dvnprodlem2  47172  itgsinexplem1  47179  stoweidlem26  47251  wallispilem5  47294  wallispi  47295  wallispi2lem1  47296  wallispi2lem2  47297  stirlinglem3  47301  stirlinglem10  47308  stirlinglem15  47313  dirkertrigeqlem1  47323  dirkertrigeqlem2  47324  dirkertrigeqlem3  47325  dirkertrigeq  47326  dirkercncflem2  47329  fourierdlem66  47397  fourierswlem  47455  fouriersw  47456  etransclem23  47482  etransclem25  47484  etransclem46  47505  hoidmvlelem2  47821  sigarls  48082  sharhght  48090  sin3t  48132  cos3t  48133  sin5tlem2  48135  sin5tlem3  48136  sin5tlem4  48137  modmkpkne  48652  fmtnorec4  48849  fmtnoprmfac2lem1  48866  fmtnoprmfac2  48867  fmtnofac2lem  48868  fmtnofac1  48870  lighneallem4a  48908  perfectALTVlem1  49034  perfectALTVlem2  49035  perfectALTV  49036  2zrngmmgm  49564  altgsumbcALT  49680  nn0sumshdiglemB  49947  affinecomb2  50030  itscnhlc0yqe  50086  itschlc0yqe  50087  itsclc0yqsollem1  50089  itsclc0yqsol  50091  itscnhlc0xyqsol  50092  itsclc0xyqsolr  50096  itsclquadb  50103  aacllem  51251  crosspdotd  51277  crossp3d  51279