Theorem mulassd 11313

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

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

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

This theorem is referenced by:  recex  11922  mulcand  11923  receu  11935  divmulasscom  11973  divdivdiv  11995  divmuleq  11999  conjmul  12011  modmul1  13975  moddi  13990  expadd  14155  mulbinom2  14272  binom3  14273  digit1  14286  discr1  14288  discr  14289  faclbnd  14339  faclbnd6  14348  bcm1k  14364  bcp1nk  14366  crre  15163  remullem  15177  amgm2  15418  iseraltlem2  15731  iseraltlem3  15732  binomlem  15877  climcndslem2  15898  pwdif  15916  geo2sum  15921  mertenslem1  15932  clim2prod  15936  fallrisefac  16073  binomfallfaclem2  16088  bpolydiflem  16102  bpoly4  16107  sinadd  16212  tanadd  16215  pwp1fsum  16439  bezoutlem3  16588  dvdsmulgcd  16603  qredeq  16704  pcaddlem  16935  prmpwdvds  16951  ablfacrp  20110  nmoco  24779  cph2ass  25266  cphipval2  25294  csbren  25452  minveclem2  25479  uniioombllem5  25641  itg1mulc  25759  mbfi1fseqlem5  25774  itgconst  25874  itgmulc2  25889  dvexp  26011  dvply1  26343  elqaalem3  26381  aalioulem1  26392  aaliou3lem2  26403  dvtaylp  26430  dvradcnv  26482  pserdvlem2  26490  tangtx  26565  tanregt0  26599  tanarg  26679  logcnlem4  26705  cxpmul  26748  dvcxp1  26800  dvcncxp1  26803  root1eq1  26816  heron  26899  quad2  26900  dcubic1lem  26904  dcubic1  26906  cubic2  26909  binom4  26911  dquartlem1  26912  dquartlem2  26913  dquart  26914  quart1lem  26916  quart1  26917  quartlem1  26918  efiasin  26949  asinsinlem  26952  asinsin  26953  efiatan  26973  efiatan2  26978  2efiatan  26979  atantan  26984  atanbndlem  26986  atans2  26992  atantayl  26998  log2cnv  27005  log2tlbnd  27006  ftalem1  27134  ftalem5  27138  basellem3  27144  basellem5  27146  basellem8  27149  chtub  27274  perfectlem1  27291  perfectlem2  27292  perfect  27293  bcmono  27339  bclbnd  27342  bposlem9  27354  lgsneg  27383  gausslemma2dlem6  27434  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgsquad2lem1  27446  lgsquad3  27449  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgsoddprmlem2  27471  2sqlem3  27482  chto1ub  27538  rplogsumlem1  27546  dchrmusum2  27556  dchrvmasum2lem  27558  dchrvmasumlem2  27560  dchrvmasumiflem2  27564  dchrisum0lem1  27578  dchrisum0lem2  27580  mulog2sumlem2  27597  chpdifbndlem1  27615  selberg3lem1  27619  selberg4lem1  27622  selberg34r  27633  pntrlog2bndlem3  27641  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntlemh  27661  pntlemr  27664  pntlemf  27667  pntlemk  27668  pntlemo  27669  colinearalglem4  28942  axpasch  28974  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  ipasslem4  30866  minvecolem2  30907  his35  31120  leopnmid  32170  quad3d  32757  zringfrac  33547  ccfldsrarelvec  33681  constrrtll  33722  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  oddpwdc  34319  prodfzo03  34580  itgexpif  34583  breprexplemc  34609  circlemeth  34617  hgt750lemg  34631  hgt750lemb  34633  hgt750leme  34635  subfacval2  35155  subfaclim  35156  circum  35642  faclimlem1  35705  faclimlem3  35707  faclim2  35710  unbdqndv2lem1  36475  knoppndvlem2  36479  knoppndvlem7  36484  knoppndvlem11  36488  knoppndvlem12  36489  knoppndvlem14  36491  knoppndvlem18  36495  itgmulc2nc  37648  areacirclem1  37668  areacirclem4  37671  bfplem1  37782  lcmineqlem1  41986  lcmineqlem5  41990  lcmineqlem10  41995  lcmineqlem12  41997  lcmineqlem18  42003  lcmineqlem20  42005  dvrelogpow2b  42025  aks4d1p1p7  42031  primrootscoprmpow  42056  2np3bcnp1  42101  remulcan2d  42252  remul02  42381  remul01  42383  sn-it0e0  42391  remulinvcom  42408  remullid  42409  sn-mullid  42411  remulcand  42414  sn-0tie0  42415  sn-mul02  42416  mulgt0b2d  42436  sn-itrere  42444  sn-retire  42445  flt4lem5e  42611  flt4lem5f  42612  fltnlta  42618  cu3addd  42636  3cubeslem2  42641  3cubeslem3l  42642  3cubeslem3r  42643  pellexlem6  42790  rmxluc  42893  rmyluc2  42895  rmydbl  42897  jm2.18  42945  jm2.23  42953  jm2.27c  42964  jm3.1lem2  42975  proot1ex  43157  sqrtcval  43603  sqrtcval2  43604  int-mulassocd  44139  binomcxplemnotnn0  44325  mul13d  45194  fmul01lt1lem1  45505  fmul01lt1lem2  45506  coskpi2  45787  cosknegpi  45790  dvnxpaek  45863  dvmptfprodlem  45865  dvnprodlem2  45868  itgsinexplem1  45875  stoweidlem26  45947  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem3  45997  stirlinglem10  46004  stirlinglem15  46009  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem2  46025  fourierdlem66  46093  fourierswlem  46151  fouriersw  46152  etransclem23  46178  etransclem25  46180  etransclem46  46201  hoidmvlelem2  46517  sigarls  46778  sharhght  46786  fmtnorec4  47423  fmtnoprmfac2lem1  47440  fmtnoprmfac2  47441  fmtnofac2lem  47442  fmtnofac1  47444  lighneallem4a  47482  perfectALTVlem1  47595  perfectALTVlem2  47596  perfectALTV  47597  2zrngmmgm  47975  altgsumbcALT  48078  nn0sumshdiglemB  48354  affinecomb2  48437  itscnhlc0yqe  48493  itschlc0yqe  48494  itsclc0yqsollem1  48496  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itsclc0xyqsolr  48503  itsclquadb  48510  aacllem  48895