Theorem mulassd 11281

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

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

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

This theorem is referenced by:  recex  11892  mulcand  11893  receu  11905  divmulasscom  11943  divdivdiv  11965  divmuleq  11969  conjmul  11981  modmul1  13961  moddi  13976  expadd  14141  mulbinom2  14258  binom3  14259  digit1  14272  discr1  14274  discr  14275  faclbnd  14325  faclbnd6  14334  bcm1k  14350  bcp1nk  14352  crre  15149  remullem  15163  amgm2  15404  iseraltlem2  15715  iseraltlem3  15716  binomlem  15861  climcndslem2  15882  pwdif  15900  geo2sum  15905  mertenslem1  15916  clim2prod  15920  fallrisefac  16057  binomfallfaclem2  16072  bpolydiflem  16086  bpoly4  16091  sinadd  16196  tanadd  16199  pwp1fsum  16424  bezoutlem3  16574  dvdsmulgcd  16589  qredeq  16690  pcaddlem  16921  prmpwdvds  16937  ablfacrp  20100  nmoco  24773  cph2ass  25260  cphipval2  25288  csbren  25446  minveclem2  25473  uniioombllem5  25635  itg1mulc  25753  mbfi1fseqlem5  25768  itgconst  25868  itgmulc2  25883  dvexp  26005  dvply1  26339  elqaalem3  26377  aalioulem1  26388  aaliou3lem2  26399  dvtaylp  26426  dvradcnv  26478  pserdvlem2  26486  tangtx  26561  tanregt0  26595  tanarg  26675  logcnlem4  26701  cxpmul  26744  dvcxp1  26796  dvcncxp1  26799  root1eq1  26812  heron  26895  quad2  26896  dcubic1lem  26900  dcubic1  26902  cubic2  26905  binom4  26907  dquartlem1  26908  dquartlem2  26909  dquart  26910  quart1lem  26912  quart1  26913  quartlem1  26914  efiasin  26945  asinsinlem  26948  asinsin  26949  efiatan  26969  efiatan2  26974  2efiatan  26975  atantan  26980  atanbndlem  26982  atans2  26988  atantayl  26994  log2cnv  27001  log2tlbnd  27002  ftalem1  27130  ftalem5  27134  basellem3  27140  basellem5  27142  basellem8  27145  chtub  27270  perfectlem1  27287  perfectlem2  27288  perfect  27289  bcmono  27335  bclbnd  27338  bposlem9  27350  lgsneg  27379  gausslemma2dlem6  27430  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgsquad2lem1  27442  lgsquad3  27445  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2lgsoddprmlem2  27467  2sqlem3  27478  chto1ub  27534  rplogsumlem1  27542  dchrmusum2  27552  dchrvmasum2lem  27554  dchrvmasumlem2  27556  dchrvmasumiflem2  27560  dchrisum0lem1  27574  dchrisum0lem2  27576  mulog2sumlem2  27593  chpdifbndlem1  27611  selberg3lem1  27615  selberg4lem1  27618  selberg34r  27629  pntrlog2bndlem3  27637  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntlemh  27657  pntlemr  27660  pntlemf  27663  pntlemk  27664  pntlemo  27665  colinearalglem4  28938  axpasch  28970  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  ipasslem4  30862  minvecolem2  30903  his35  31116  leopnmid  32166  quad3d  32760  zringfrac  33561  ccfldsrarelvec  33695  constrrtll  33736  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  oddpwdc  34335  prodfzo03  34596  itgexpif  34599  breprexplemc  34625  circlemeth  34633  hgt750lemg  34647  hgt750lemb  34649  hgt750leme  34651  subfacval2  35171  subfaclim  35172  circum  35658  faclimlem1  35722  faclimlem3  35724  faclim2  35727  unbdqndv2lem1  36491  knoppndvlem2  36495  knoppndvlem7  36500  knoppndvlem11  36504  knoppndvlem12  36505  knoppndvlem14  36507  knoppndvlem18  36511  itgmulc2nc  37674  areacirclem1  37694  areacirclem4  37697  bfplem1  37808  lcmineqlem1  42010  lcmineqlem5  42014  lcmineqlem10  42019  lcmineqlem12  42021  lcmineqlem18  42027  lcmineqlem20  42029  dvrelogpow2b  42049  aks4d1p1p7  42055  primrootscoprmpow  42080  2np3bcnp1  42125  remulcan2d  42276  remul02  42411  remul01  42413  sn-it0e0  42421  remulinvcom  42438  remullid  42439  sn-mullid  42441  remulcand  42444  sn-0tie0  42445  sn-mul02  42446  mulgt0b2d  42466  sn-itrere  42474  sn-retire  42475  flt4lem5e  42642  flt4lem5f  42643  fltnlta  42649  cu3addd  42667  3cubeslem2  42672  3cubeslem3l  42673  3cubeslem3r  42674  pellexlem6  42821  rmxluc  42924  rmyluc2  42926  rmydbl  42928  jm2.18  42976  jm2.23  42984  jm2.27c  42995  jm3.1lem2  43006  proot1ex  43184  sqrtcval  43630  sqrtcval2  43631  int-mulassocd  44166  binomcxplemnotnn0  44351  mul13d  45229  fmul01lt1lem1  45539  fmul01lt1lem2  45540  coskpi2  45821  cosknegpi  45824  dvnxpaek  45897  dvmptfprodlem  45899  dvnprodlem2  45902  itgsinexplem1  45909  stoweidlem26  45981  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem3  46031  stirlinglem10  46038  stirlinglem15  46043  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem2  46059  fourierdlem66  46127  fourierswlem  46185  fouriersw  46186  etransclem23  46212  etransclem25  46214  etransclem46  46235  hoidmvlelem2  46551  sigarls  46812  sharhght  46820  fmtnorec4  47473  fmtnoprmfac2lem1  47490  fmtnoprmfac2  47491  fmtnofac2lem  47492  fmtnofac1  47494  lighneallem4a  47532  perfectALTVlem1  47645  perfectALTVlem2  47646  perfectALTV  47647  2zrngmmgm  48095  altgsumbcALT  48197  nn0sumshdiglemB  48469  affinecomb2  48552  itscnhlc0yqe  48608  itschlc0yqe  48609  itsclc0yqsollem1  48611  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itsclc0xyqsolr  48618  itsclquadb  48625  aacllem  49031