Theorem mulassd 11241

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   · cmul 11117

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087

This theorem is referenced by:  recex  11850  mulcand  11851  receu  11863  divmulasscom  11900  divdivdiv  11919  divmuleq  11923  conjmul  11935  modmul1  13893  moddi  13908  expadd  14074  mulbinom2  14190  binom3  14191  digit1  14204  discr1  14206  discr  14207  faclbnd  14254  faclbnd6  14263  bcm1k  14279  bcp1nk  14281  crre  15065  remullem  15079  amgm2  15320  iseraltlem2  15633  iseraltlem3  15634  binomlem  15779  climcndslem2  15800  pwdif  15818  geo2sum  15823  mertenslem1  15834  clim2prod  15838  fallrisefac  15973  binomfallfaclem2  15988  bpolydiflem  16002  bpoly4  16007  sinadd  16111  tanadd  16114  pwp1fsum  16338  bezoutlem3  16487  dvdsmulgcd  16501  qredeq  16598  pcaddlem  16825  prmpwdvds  16841  ablfacrp  19977  nmoco  24474  cph2ass  24961  cphipval2  24989  csbren  25147  minveclem2  25174  uniioombllem5  25336  itg1mulc  25454  mbfi1fseqlem5  25469  itgconst  25568  itgmulc2  25583  dvexp  25705  dvply1  26033  elqaalem3  26070  aalioulem1  26081  aaliou3lem2  26092  dvtaylp  26118  dvradcnv  26169  pserdvlem2  26176  tangtx  26251  tanregt0  26284  tanarg  26363  logcnlem4  26389  cxpmul  26432  dvcxp1  26484  dvcncxp1  26487  root1eq1  26499  heron  26579  quad2  26580  dcubic1lem  26584  dcubic1  26586  cubic2  26589  binom4  26591  dquartlem1  26592  dquartlem2  26593  dquart  26594  quart1lem  26596  quart1  26597  quartlem1  26598  efiasin  26629  asinsinlem  26632  asinsin  26633  efiatan  26653  efiatan2  26658  2efiatan  26659  atantan  26664  atanbndlem  26666  atans2  26672  atantayl  26678  log2cnv  26685  log2tlbnd  26686  ftalem1  26813  ftalem5  26817  basellem3  26823  basellem5  26825  basellem8  26828  chtub  26951  perfectlem1  26968  perfectlem2  26969  perfect  26970  bcmono  27016  bclbnd  27019  bposlem9  27031  lgsneg  27060  gausslemma2dlem6  27111  lgseisenlem1  27114  lgseisenlem2  27115  lgseisenlem3  27116  lgseisenlem4  27117  lgsquad2lem1  27123  lgsquad3  27126  2lgslem3a  27135  2lgslem3b  27136  2lgslem3c  27137  2lgslem3d  27138  2lgsoddprmlem2  27148  2sqlem3  27159  chto1ub  27215  rplogsumlem1  27223  dchrmusum2  27233  dchrvmasum2lem  27235  dchrvmasumlem2  27237  dchrvmasumiflem2  27241  dchrisum0lem1  27255  dchrisum0lem2  27257  mulog2sumlem2  27274  chpdifbndlem1  27292  selberg3lem1  27296  selberg4lem1  27299  selberg34r  27310  pntrlog2bndlem3  27318  pntrlog2bndlem5  27320  pntrlog2bndlem6  27322  pntlemh  27338  pntlemr  27341  pntlemf  27344  pntlemk  27345  pntlemo  27346  colinearalglem4  28434  axpasch  28466  axcontlem2  28490  axcontlem4  28492  axcontlem7  28495  axcontlem8  28496  ipasslem4  30354  minvecolem2  30395  his35  30608  leopnmid  31658  ccfldsrarelvec  33034  oddpwdc  33651  prodfzo03  33913  itgexpif  33916  breprexplemc  33942  circlemeth  33950  hgt750lemg  33964  hgt750lemb  33966  hgt750leme  33968  subfacval2  34476  subfaclim  34477  circum  34957  faclimlem1  35017  faclimlem3  35019  faclim2  35022  unbdqndv2lem1  35688  knoppndvlem2  35692  knoppndvlem7  35697  knoppndvlem11  35701  knoppndvlem12  35702  knoppndvlem14  35704  knoppndvlem18  35708  itgmulc2nc  36859  areacirclem1  36879  areacirclem4  36882  bfplem1  36993  lcmineqlem1  41200  lcmineqlem5  41204  lcmineqlem10  41209  lcmineqlem12  41211  lcmineqlem18  41217  lcmineqlem20  41219  dvrelogpow2b  41239  aks4d1p1p7  41245  2np3bcnp1  41266  remulcan2d  41479  remul02  41580  remul01  41582  sn-it0e0  41590  remulinvcom  41607  remullid  41608  sn-mullid  41610  remulcand  41613  sn-0tie0  41614  sn-mul02  41615  mulgt0b2d  41635  itrere  41641  retire  41642  flt4lem5e  41700  flt4lem5f  41701  fltnlta  41707  cu3addd  41720  3cubeslem2  41725  3cubeslem3l  41726  3cubeslem3r  41727  pellexlem6  41874  rmxluc  41977  rmyluc2  41979  rmydbl  41981  jm2.18  42029  jm2.23  42037  jm2.27c  42048  jm3.1lem2  42059  proot1ex  42245  sqrtcval  42694  sqrtcval2  42695  int-mulassocd  43231  binomcxplemnotnn0  43417  mul13d  44287  fmul01lt1lem1  44598  fmul01lt1lem2  44599  coskpi2  44880  cosknegpi  44883  dvnxpaek  44956  dvmptfprodlem  44958  dvnprodlem2  44961  itgsinexplem1  44968  stoweidlem26  45040  wallispilem5  45083  wallispi  45084  wallispi2lem1  45085  wallispi2lem2  45086  stirlinglem3  45090  stirlinglem10  45097  stirlinglem15  45102  dirkertrigeqlem1  45112  dirkertrigeqlem2  45113  dirkertrigeqlem3  45114  dirkertrigeq  45115  dirkercncflem2  45118  fourierdlem66  45186  fourierswlem  45244  fouriersw  45245  etransclem23  45271  etransclem25  45273  etransclem46  45294  hoidmvlelem2  45610  sigarls  45871  sharhght  45879  fmtnorec4  46515  fmtnoprmfac2lem1  46532  fmtnoprmfac2  46533  fmtnofac2lem  46534  fmtnofac1  46536  lighneallem4a  46574  perfectALTVlem1  46687  perfectALTVlem2  46688  perfectALTV  46689  2zrngmmgm  46932  altgsumbcALT  47117  nn0sumshdiglemB  47393  affinecomb2  47476  itscnhlc0yqe  47532  itschlc0yqe  47533  itsclc0yqsollem1  47535  itsclc0yqsol  47537  itscnhlc0xyqsol  47538  itsclc0xyqsolr  47542  itsclquadb  47549  aacllem  47935