Theorem mulassd 11284

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

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

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

This theorem is referenced by:  recex  11895  mulcand  11896  receu  11908  divmulasscom  11946  divdivdiv  11968  divmuleq  11972  conjmul  11984  modmul1  13965  moddi  13980  expadd  14145  mulbinom2  14262  binom3  14263  digit1  14276  discr1  14278  discr  14279  faclbnd  14329  faclbnd6  14338  bcm1k  14354  bcp1nk  14356  crre  15153  remullem  15167  amgm2  15408  iseraltlem2  15719  iseraltlem3  15720  binomlem  15865  climcndslem2  15886  pwdif  15904  geo2sum  15909  mertenslem1  15920  clim2prod  15924  fallrisefac  16061  binomfallfaclem2  16076  bpolydiflem  16090  bpoly4  16095  sinadd  16200  tanadd  16203  pwp1fsum  16428  bezoutlem3  16578  dvdsmulgcd  16593  qredeq  16694  pcaddlem  16926  prmpwdvds  16942  ablfacrp  20086  nmoco  24758  cph2ass  25247  cphipval2  25275  csbren  25433  minveclem2  25460  uniioombllem5  25622  itg1mulc  25739  mbfi1fseqlem5  25754  itgconst  25854  itgmulc2  25869  dvexp  25991  dvply1  26325  elqaalem3  26363  aalioulem1  26374  aaliou3lem2  26385  dvtaylp  26412  dvradcnv  26464  pserdvlem2  26472  tangtx  26547  tanregt0  26581  tanarg  26661  logcnlem4  26687  cxpmul  26730  dvcxp1  26782  dvcncxp1  26785  root1eq1  26798  heron  26881  quad2  26882  dcubic1lem  26886  dcubic1  26888  cubic2  26891  binom4  26893  dquartlem1  26894  dquartlem2  26895  dquart  26896  quart1lem  26898  quart1  26899  quartlem1  26900  efiasin  26931  asinsinlem  26934  asinsin  26935  efiatan  26955  efiatan2  26960  2efiatan  26961  atantan  26966  atanbndlem  26968  atans2  26974  atantayl  26980  log2cnv  26987  log2tlbnd  26988  ftalem1  27116  ftalem5  27120  basellem3  27126  basellem5  27128  basellem8  27131  chtub  27256  perfectlem1  27273  perfectlem2  27274  perfect  27275  bcmono  27321  bclbnd  27324  bposlem9  27336  lgsneg  27365  gausslemma2dlem6  27416  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgsquad2lem1  27428  lgsquad3  27431  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgsoddprmlem2  27453  2sqlem3  27464  chto1ub  27520  rplogsumlem1  27528  dchrmusum2  27538  dchrvmasum2lem  27540  dchrvmasumlem2  27542  dchrvmasumiflem2  27546  dchrisum0lem1  27560  dchrisum0lem2  27562  mulog2sumlem2  27579  chpdifbndlem1  27597  selberg3lem1  27601  selberg4lem1  27604  selberg34r  27615  pntrlog2bndlem3  27623  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntlemh  27643  pntlemr  27646  pntlemf  27649  pntlemk  27650  pntlemo  27651  colinearalglem4  28924  axpasch  28956  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  ipasslem4  30853  minvecolem2  30894  his35  31107  leopnmid  32157  quad3d  32754  zringfrac  33582  ccfldsrarelvec  33721  constrrtll  33772  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  oddpwdc  34356  prodfzo03  34618  itgexpif  34621  breprexplemc  34647  circlemeth  34655  hgt750lemg  34669  hgt750lemb  34671  hgt750leme  34673  subfacval2  35192  subfaclim  35193  circum  35679  faclimlem1  35743  faclimlem3  35745  faclim2  35748  unbdqndv2lem1  36510  knoppndvlem2  36514  knoppndvlem7  36519  knoppndvlem11  36523  knoppndvlem12  36524  knoppndvlem14  36526  knoppndvlem18  36530  itgmulc2nc  37695  areacirclem1  37715  areacirclem4  37718  bfplem1  37829  lcmineqlem1  42030  lcmineqlem5  42034  lcmineqlem10  42039  lcmineqlem12  42041  lcmineqlem18  42047  lcmineqlem20  42049  dvrelogpow2b  42069  aks4d1p1p7  42075  primrootscoprmpow  42100  2np3bcnp1  42145  remulcan2d  42298  remul02  42435  remul01  42437  sn-it0e0  42445  remulinvcom  42462  remullid  42463  sn-mullid  42465  remulcand  42468  sn-0tie0  42469  sn-mul02  42470  mulgt0b2d  42490  sn-itrere  42498  sn-retire  42499  flt4lem5e  42666  flt4lem5f  42667  fltnlta  42673  cu3addd  42691  3cubeslem2  42696  3cubeslem3l  42697  3cubeslem3r  42698  pellexlem6  42845  rmxluc  42948  rmyluc2  42950  rmydbl  42952  jm2.18  43000  jm2.23  43008  jm2.27c  43019  jm3.1lem2  43030  proot1ex  43208  sqrtcval  43654  sqrtcval2  43655  int-mulassocd  44190  binomcxplemnotnn0  44375  mul13d  45291  fmul01lt1lem1  45599  fmul01lt1lem2  45600  coskpi2  45881  cosknegpi  45884  dvnxpaek  45957  dvmptfprodlem  45959  dvnprodlem2  45962  itgsinexplem1  45969  stoweidlem26  46041  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem3  46091  stirlinglem10  46098  stirlinglem15  46103  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem2  46119  fourierdlem66  46187  fourierswlem  46245  fouriersw  46246  etransclem23  46272  etransclem25  46274  etransclem46  46295  hoidmvlelem2  46611  sigarls  46872  sharhght  46880  fmtnorec4  47536  fmtnoprmfac2lem1  47553  fmtnoprmfac2  47554  fmtnofac2lem  47555  fmtnofac1  47557  lighneallem4a  47595  perfectALTVlem1  47708  perfectALTVlem2  47709  perfectALTV  47710  2zrngmmgm  48168  altgsumbcALT  48269  nn0sumshdiglemB  48541  affinecomb2  48624  itscnhlc0yqe  48680  itschlc0yqe  48681  itsclc0yqsollem1  48683  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itsclc0xyqsolr  48690  itsclquadb  48697  aacllem  49320