Theorem mulassd 11220

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

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

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

This theorem is referenced by:  recex  11834  mulcand  11835  receu  11847  divmulasscom  11884  divdivdiv  11907  divmuleq  11911  conjmul  11923  modmul1  13951  moddi  13966  expadd  14131  mulbinom2  14250  binom3  14251  digit1  14264  discr1  14266  discr  14267  faclbnd  14317  faclbnd6  14326  bcm1k  14342  bcp1nk  14344  crre  15155  remullem  15169  amgm2  15411  iseraltlem2  15724  iseraltlem3  15725  binomlem  15873  climcndslem2  15894  pwdif  15912  geo2sum  15917  mertenslem1  15928  clim2prod  15932  fallrisefac  16069  binomfallfaclem2  16084  bpolydiflem  16098  bpoly4  16103  sinadd  16210  tanadd  16213  pwp1fsum  16439  bezoutlem3  16589  dvdsmulgcd  16604  qredeq  16705  pcaddlem  16938  prmpwdvds  16954  ablfacrp  20129  nmoco  24855  cph2ass  25333  cphipval2  25361  csbren  25519  minveclem2  25546  uniioombllem5  25707  itg1mulc  25824  mbfi1fseqlem5  25839  itgconst  25939  itgmulc2  25954  dvexp  26073  dvply1  26406  elqaalem3  26443  aalioulem1  26454  aaliou3lem2  26465  dvtaylp  26491  dvradcnv  26542  pserdvlem2  26549  tangtx  26628  tanregt0  26662  tanarg  26742  logcnlem4  26768  cxpmul  26811  dvcxp1  26863  dvcncxp1  26866  root1eq1  26878  heron  26961  quad2  26962  dcubic1lem  26966  dcubic1  26968  cubic2  26971  binom4  26973  dquartlem1  26974  dquartlem2  26975  dquart  26976  quart1lem  26978  quart1  26979  quartlem1  26980  efiasin  27011  asinsinlem  27014  asinsin  27015  efiatan  27035  efiatan2  27040  2efiatan  27041  atantan  27046  atanbndlem  27048  atans2  27054  atantayl  27060  log2cnv  27067  log2tlbnd  27068  ftalem1  27195  ftalem5  27199  basellem3  27205  basellem5  27207  basellem8  27210  chtub  27334  perfectlem1  27351  perfectlem2  27352  perfect  27353  bcmono  27399  bclbnd  27402  bposlem9  27414  lgsneg  27443  gausslemma2dlem6  27494  lgseisenlem1  27497  lgseisenlem2  27498  lgseisenlem3  27499  lgseisenlem4  27500  lgsquad2lem1  27506  lgsquad3  27509  2lgslem3a  27518  2lgslem3b  27519  2lgslem3c  27520  2lgslem3d  27521  2lgsoddprmlem2  27531  2sqlem3  27542  chto1ub  27598  rplogsumlem1  27606  dchrmusum2  27616  dchrvmasum2lem  27618  dchrvmasumlem2  27620  dchrvmasumiflem2  27624  dchrisum0lem1  27638  dchrisum0lem2  27640  mulog2sumlem2  27657  chpdifbndlem1  27675  selberg3lem1  27679  selberg4lem1  27682  selberg34r  27693  pntrlog2bndlem3  27701  pntrlog2bndlem5  27703  pntrlog2bndlem6  27705  pntlemh  27721  pntlemr  27724  pntlemf  27727  pntlemk  27728  pntlemo  27729  colinearalglem4  29168  axpasch  29200  axcontlem2  29224  axcontlem4  29226  axcontlem7  29229  axcontlem8  29230  ipasslem4  31095  minvecolem2  31136  his35  31349  leopnmid  32399  quad3d  33006  zringfrac  33761  ccfldsrarelvec  33978  constrrtll  34038  constrrtlc1  34039  constrrtcclem  34041  constrrtcc  34042  cos9thpiminplylem2  34090  oddpwdc  34661  prodfzo03  34907  itgexpif  34910  breprexplemc  34936  circlemeth  34944  hgt750lemg  34958  hgt750lemb  34960  hgt750leme  34962  subfacval2  35550  subfaclim  35551  circum  36037  faclimlem1  36106  faclimlem3  36108  faclim2  36111  unbdqndv2lem1  36960  knoppndvlem2  36964  knoppndvlem7  36969  knoppndvlem11  36973  knoppndvlem12  36974  knoppndvlem14  36976  knoppndvlem18  36980  itgmulc2nc  38199  areacirclem1  38219  areacirclem4  38222  bfplem1  38333  lcmineqlem1  42658  lcmineqlem5  42662  lcmineqlem10  42667  lcmineqlem12  42669  lcmineqlem18  42675  lcmineqlem20  42677  dvrelogpow2b  42697  aks4d1p1p7  42703  primrootscoprmpow  42728  2np3bcnp1  42773  remulcan2d  42884  remul02  43026  remul01  43028  sn-it0e0  43037  remulinvcom  43054  remullid  43055  sn-mullid  43057  remulcand  43060  rediveud  43064  redivrec2d  43081  rediv23d  43082  sn-0tie0  43085  sn-mul02  43086  mulgt0b1d  43106  mulgt0b2d  43112  mullt0b1d  43117  sn-itrere  43122  sn-retire  43123  flt4lem5e  43250  flt4lem5f  43251  fltnlta  43257  cu3addd  43274  3cubeslem2  43278  3cubeslem3l  43279  3cubeslem3r  43280  pellexlem6  43423  rmxluc  43525  rmyluc2  43527  rmydbl  43529  jm2.18  43577  jm2.23  43585  jm2.27c  43596  jm3.1lem2  43607  proot1ex  43785  sqrtcval  44229  sqrtcval2  44230  int-mulassocd  44765  binomcxplemnotnn0  44930  mul13d  45857  fmul01lt1lem1  46158  fmul01lt1lem2  46159  coskpi2  46438  cosknegpi  46441  dvnxpaek  46514  dvmptfprodlem  46516  dvnprodlem2  46519  itgsinexplem1  46526  stoweidlem26  46598  wallispilem5  46641  wallispi  46642  wallispi2lem1  46643  wallispi2lem2  46644  stirlinglem3  46648  stirlinglem10  46655  stirlinglem15  46660  dirkertrigeqlem1  46670  dirkertrigeqlem2  46671  dirkertrigeqlem3  46672  dirkertrigeq  46673  dirkercncflem2  46676  fourierdlem66  46744  fourierswlem  46802  fouriersw  46803  etransclem23  46829  etransclem25  46831  etransclem46  46852  hoidmvlelem2  47168  sigarls  47429  sharhght  47437  sin3t  47463  cos3t  47464  sin5tlem2  47466  sin5tlem3  47467  sin5tlem4  47468  modmkpkne  47959  fmtnorec4  48156  fmtnoprmfac2lem1  48173  fmtnoprmfac2  48174  fmtnofac2lem  48175  fmtnofac1  48177  lighneallem4a  48215  perfectALTVlem1  48341  perfectALTVlem2  48342  perfectALTV  48343  2zrngmmgm  48872  altgsumbcALT  48984  nn0sumshdiglemB  49251  affinecomb2  49334  itscnhlc0yqe  49390  itschlc0yqe  49391  itsclc0yqsollem1  49393  itsclc0yqsol  49395  itscnhlc0xyqsol  49396  itsclc0xyqsolr  49400  itsclquadb  49407  aacllem  50430