Theorem mulassd 11157

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  recex  11770  mulcand  11771  receu  11783  divmulasscom  11821  divdivdiv  11843  divmuleq  11847  conjmul  11859  modmul1  13849  moddi  13864  expadd  14029  mulbinom2  14148  binom3  14149  digit1  14162  discr1  14164  discr  14165  faclbnd  14215  faclbnd6  14224  bcm1k  14240  bcp1nk  14242  crre  15039  remullem  15053  amgm2  15295  iseraltlem2  15608  iseraltlem3  15609  binomlem  15754  climcndslem2  15775  pwdif  15793  geo2sum  15798  mertenslem1  15809  clim2prod  15813  fallrisefac  15950  binomfallfaclem2  15965  bpolydiflem  15979  bpoly4  15984  sinadd  16091  tanadd  16094  pwp1fsum  16320  bezoutlem3  16470  dvdsmulgcd  16485  qredeq  16586  pcaddlem  16818  prmpwdvds  16834  ablfacrp  19965  nmoco  24641  cph2ass  25129  cphipval2  25157  csbren  25315  minveclem2  25342  uniioombllem5  25504  itg1mulc  25621  mbfi1fseqlem5  25636  itgconst  25736  itgmulc2  25751  dvexp  25873  dvply1  26207  elqaalem3  26245  aalioulem1  26256  aaliou3lem2  26267  dvtaylp  26294  dvradcnv  26346  pserdvlem2  26354  tangtx  26430  tanregt0  26464  tanarg  26544  logcnlem4  26570  cxpmul  26613  dvcxp1  26665  dvcncxp1  26668  root1eq1  26681  heron  26764  quad2  26765  dcubic1lem  26769  dcubic1  26771  cubic2  26774  binom4  26776  dquartlem1  26777  dquartlem2  26778  dquart  26779  quart1lem  26781  quart1  26782  quartlem1  26783  efiasin  26814  asinsinlem  26817  asinsin  26818  efiatan  26838  efiatan2  26843  2efiatan  26844  atantan  26849  atanbndlem  26851  atans2  26857  atantayl  26863  log2cnv  26870  log2tlbnd  26871  ftalem1  26999  ftalem5  27003  basellem3  27009  basellem5  27011  basellem8  27014  chtub  27139  perfectlem1  27156  perfectlem2  27157  perfect  27158  bcmono  27204  bclbnd  27207  bposlem9  27219  lgsneg  27248  gausslemma2dlem6  27299  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgseisenlem4  27305  lgsquad2lem1  27311  lgsquad3  27314  2lgslem3a  27323  2lgslem3b  27324  2lgslem3c  27325  2lgslem3d  27326  2lgsoddprmlem2  27336  2sqlem3  27347  chto1ub  27403  rplogsumlem1  27411  dchrmusum2  27421  dchrvmasum2lem  27423  dchrvmasumlem2  27425  dchrvmasumiflem2  27429  dchrisum0lem1  27443  dchrisum0lem2  27445  mulog2sumlem2  27462  chpdifbndlem1  27480  selberg3lem1  27484  selberg4lem1  27487  selberg34r  27498  pntrlog2bndlem3  27506  pntrlog2bndlem5  27508  pntrlog2bndlem6  27510  pntlemh  27526  pntlemr  27529  pntlemf  27532  pntlemk  27533  pntlemo  27534  colinearalglem4  28872  axpasch  28904  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  axcontlem8  28934  ipasslem4  30796  minvecolem2  30837  his35  31050  leopnmid  32100  quad3d  32706  zringfrac  33501  ccfldsrarelvec  33642  constrrtll  33697  constrrtlc1  33698  constrrtcclem  33700  constrrtcc  33701  cos9thpiminplylem2  33749  oddpwdc  34321  prodfzo03  34570  itgexpif  34573  breprexplemc  34599  circlemeth  34607  hgt750lemg  34621  hgt750lemb  34623  hgt750leme  34625  subfacval2  35159  subfaclim  35160  circum  35646  faclimlem1  35715  faclimlem3  35717  faclim2  35720  unbdqndv2lem1  36482  knoppndvlem2  36486  knoppndvlem7  36491  knoppndvlem11  36495  knoppndvlem12  36496  knoppndvlem14  36498  knoppndvlem18  36502  itgmulc2nc  37667  areacirclem1  37687  areacirclem4  37690  bfplem1  37801  lcmineqlem1  42002  lcmineqlem5  42006  lcmineqlem10  42011  lcmineqlem12  42013  lcmineqlem18  42019  lcmineqlem20  42021  dvrelogpow2b  42041  aks4d1p1p7  42047  primrootscoprmpow  42072  2np3bcnp1  42117  remulcan2d  42230  remul02  42378  remul01  42380  sn-it0e0  42389  remulinvcom  42406  remullid  42407  sn-mullid  42409  remulcand  42412  rediveud  42416  sn-0tie0  42424  sn-mul02  42425  mulgt0b1d  42445  mulgt0b2d  42451  mullt0b1d  42456  sn-itrere  42461  sn-retire  42462  flt4lem5e  42629  flt4lem5f  42630  fltnlta  42636  cu3addd  42654  3cubeslem2  42658  3cubeslem3l  42659  3cubeslem3r  42660  pellexlem6  42807  rmxluc  42909  rmyluc2  42911  rmydbl  42913  jm2.18  42961  jm2.23  42969  jm2.27c  42980  jm3.1lem2  42991  proot1ex  43169  sqrtcval  43614  sqrtcval2  43615  int-mulassocd  44150  binomcxplemnotnn0  44329  mul13d  45262  fmul01lt1lem1  45566  fmul01lt1lem2  45567  coskpi2  45848  cosknegpi  45851  dvnxpaek  45924  dvmptfprodlem  45926  dvnprodlem2  45929  itgsinexplem1  45936  stoweidlem26  46008  wallispilem5  46051  wallispi  46052  wallispi2lem1  46053  wallispi2lem2  46054  stirlinglem3  46058  stirlinglem10  46065  stirlinglem15  46070  dirkertrigeqlem1  46080  dirkertrigeqlem2  46081  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem2  46086  fourierdlem66  46154  fourierswlem  46212  fouriersw  46213  etransclem23  46239  etransclem25  46241  etransclem46  46262  hoidmvlelem2  46578  sigarls  46839  sharhght  46847  modmkpkne  47346  fmtnorec4  47534  fmtnoprmfac2lem1  47551  fmtnoprmfac2  47552  fmtnofac2lem  47553  fmtnofac1  47555  lighneallem4a  47593  perfectALTVlem1  47706  perfectALTVlem2  47707  perfectALTV  47708  2zrngmmgm  48237  altgsumbcALT  48338  nn0sumshdiglemB  48606  affinecomb2  48689  itscnhlc0yqe  48745  itschlc0yqe  48746  itsclc0yqsollem1  48748  itsclc0yqsol  48750  itscnhlc0xyqsol  48751  itsclc0xyqsolr  48755  itsclquadb  48762  aacllem  49787