Theorem mulassd 11250

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   · cmul 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  recex  11864  mulcand  11865  receu  11877  divmulasscom  11914  divdivdiv  11934  divmuleq  11938  conjmul  11950  modmul1  13980  moddi  13995  expadd  14160  mulbinom2  14279  binom3  14280  digit1  14293  discr1  14295  discr  14296  faclbnd  14346  faclbnd6  14355  bcm1k  14371  bcp1nk  14373  crre  15191  remullem  15205  amgm2  15447  iseraltlem2  15760  iseraltlem3  15761  binomlem  15909  climcndslem2  15930  pwdif  15948  geo2sum  15953  mertenslem1  15964  clim2prod  15968  fallrisefac  16105  binomfallfaclem2  16119  bpolydiflem  16133  bpoly4  16138  sinadd  16245  tanadd  16248  pwp1fsum  16474  bezoutlem3  16624  dvdsmulgcd  16639  qredeq  16740  pcaddlem  16973  prmpwdvds  16989  ablfacrp  20169  nmoco  24931  cph2ass  25409  cphipval2  25437  csbren  25595  minveclem2  25622  uniioombllem5  25783  itg1mulc  25900  mbfi1fseqlem5  25915  itgconst  26015  itgmulc2  26030  dvexp  26149  dvply1  26482  elqaalem3  26519  aalioulem1  26532  aaliou3lem2  26543  dvtaylp  26570  dvradcnv  26621  pserdvlem2  26628  tangtx  26707  tanregt0  26741  tanarg  26821  logcnlem4  26847  cxpmul  26890  dvcxp1  26942  dvcncxp1  26945  root1eq1  26957  heron  27040  quad2  27041  dcubic1lem  27045  dcubic1  27047  cubic2  27050  binom4  27052  dquartlem1  27053  dquartlem2  27054  dquart  27055  quart1lem  27057  quart1  27058  quartlem1  27059  efiasin  27090  asinsinlem  27093  asinsin  27094  efiatan  27114  efiatan2  27119  2efiatan  27120  atantan  27125  atanbndlem  27127  atans2  27133  atantayl  27139  log2cnv  27146  log2tlbnd  27147  ftalem1  27274  ftalem5  27278  basellem3  27284  basellem5  27286  basellem8  27289  chtub  27413  perfectlem1  27430  perfectlem2  27431  perfect  27432  bcmono  27478  bclbnd  27481  bposlem9  27493  lgsneg  27522  gausslemma2dlem6  27573  lgseisenlem1  27576  lgseisenlem2  27577  lgseisenlem3  27578  lgseisenlem4  27579  lgsquad2lem1  27585  lgsquad3  27588  2lgslem3a  27597  2lgslem3b  27598  2lgslem3c  27599  2lgslem3d  27600  2lgsoddprmlem2  27610  2sqlem3  27621  chto1ub  27677  rplogsumlem1  27685  dchrmusum2  27695  dchrvmasum2lem  27697  dchrvmasumlem2  27699  dchrvmasumiflem2  27703  dchrisum0lem1  27717  dchrisum0lem2  27719  mulog2sumlem2  27736  chpdifbndlem1  27754  selberg3lem1  27758  selberg4lem1  27761  selberg34r  27772  pntrlog2bndlem3  27780  pntrlog2bndlem5  27782  pntrlog2bndlem6  27784  pntlemh  27800  pntlemr  27803  pntlemf  27806  pntlemk  27807  pntlemo  27808  colinearalglem4  29296  axpasch  29328  axcontlem2  29352  axcontlem4  29354  axcontlem7  29357  axcontlem8  29358  ipasslem4  31223  minvecolem2  31264  his35  31477  leopnmid  32527  quad3d  33131  zringfrac  33875  ccfldsrarelvec  34092  constrrtll  34152  constrrtlc1  34153  constrrtcclem  34155  constrrtcc  34156  cos9thpiminplylem2  34204  oddpwdc  34776  prodfzo03  35022  itgexpif  35025  breprexplemc  35051  circlemeth  35059  hgt750lemg  35073  hgt750lemb  35075  hgt750leme  35077  subfacval2  35700  subfaclim  35701  circum  36187  faclimlem1  36256  faclimlem3  36258  faclim2  36261  unbdqndv2lem1  37139  knoppndvlem2  37143  knoppndvlem7  37148  knoppndvlem11  37152  knoppndvlem12  37153  knoppndvlem14  37155  knoppndvlem18  37159  itgmulc2nc  38380  areacirclem1  38400  areacirclem4  38403  bfplem1  38514  lcmineqlem1  42837  lcmineqlem5  42841  lcmineqlem10  42846  lcmineqlem12  42848  lcmineqlem18  42854  lcmineqlem20  42856  dvrelogpow2b  42876  aks4d1p1p7  42882  primrootscoprmpow  42907  2np3bcnp1  42952  quadfac  43013  remulcan2d  43065  remul02  43207  remul01  43209  sn-it0e0  43218  remulinvcom  43235  remullid  43236  sn-mullid  43238  remulcand  43241  rediveud  43245  redivrec2d  43262  rediv23d  43263  sn-0tie0  43266  sn-mul02  43267  mulgt0b1d  43287  mulgt0b2d  43293  mullt0b1d  43298  sn-itrere  43303  sn-retire  43304  flt4lem5e  43429  flt4lem5f  43430  fltnlta  43436  cu3addd  43453  3cubeslem2  43457  3cubeslem3l  43458  3cubeslem3r  43459  pellexlem6  43602  rmxluc  43704  rmyluc2  43706  rmydbl  43708  jm2.18  43756  jm2.23  43764  jm2.27c  43775  jm3.1lem2  43786  proot1ex  43964  sqrtcval  44408  sqrtcval2  44409  int-mulassocd  44944  binomcxplemnotnn0  45107  mul13d  46040  fmul01lt1lem1  46341  fmul01lt1lem2  46342  coskpi2  46621  cosknegpi  46624  dvnxpaek  46697  dvmptfprodlem  46699  dvnprodlem2  46702  itgsinexplem1  46709  stoweidlem26  46781  wallispilem5  46824  wallispi  46825  wallispi2lem1  46826  wallispi2lem2  46827  stirlinglem3  46831  stirlinglem10  46838  stirlinglem15  46843  dirkertrigeqlem1  46853  dirkertrigeqlem2  46854  dirkertrigeqlem3  46855  dirkertrigeq  46856  dirkercncflem2  46859  fourierdlem66  46927  fourierswlem  46985  fouriersw  46986  etransclem23  47012  etransclem25  47014  etransclem46  47035  hoidmvlelem2  47351  sigarls  47612  sharhght  47620  sin3t  47649  cos3t  47650  sin5tlem2  47652  sin5tlem3  47653  sin5tlem4  47654  modmkpkne  48145  fmtnorec4  48342  fmtnoprmfac2lem1  48359  fmtnoprmfac2  48360  fmtnofac2lem  48361  fmtnofac1  48363  lighneallem4a  48401  perfectALTVlem1  48527  perfectALTVlem2  48528  perfectALTV  48529  2zrngmmgm  49058  altgsumbcALT  49174  nn0sumshdiglemB  49441  affinecomb2  49524  itscnhlc0yqe  49580  itschlc0yqe  49581  itsclc0yqsollem1  49583  itsclc0yqsol  49585  itscnhlc0xyqsol  49586  itsclc0xyqsolr  49590  itsclquadb  49597  aacllem  50662  crossp3i  50690