Theorem mulassd 11142

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   · cmul 11018

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

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

This theorem is referenced by:  recex  11756  mulcand  11757  receu  11769  divmulasscom  11807  divdivdiv  11829  divmuleq  11833  conjmul  11845  modmul1  13833  moddi  13848  expadd  14013  mulbinom2  14132  binom3  14133  digit1  14146  discr1  14148  discr  14149  faclbnd  14199  faclbnd6  14208  bcm1k  14224  bcp1nk  14226  crre  15023  remullem  15037  amgm2  15279  iseraltlem2  15592  iseraltlem3  15593  binomlem  15738  climcndslem2  15759  pwdif  15777  geo2sum  15782  mertenslem1  15793  clim2prod  15797  fallrisefac  15934  binomfallfaclem2  15949  bpolydiflem  15963  bpoly4  15968  sinadd  16075  tanadd  16078  pwp1fsum  16304  bezoutlem3  16454  dvdsmulgcd  16469  qredeq  16570  pcaddlem  16802  prmpwdvds  16818  ablfacrp  19982  nmoco  24653  cph2ass  25141  cphipval2  25169  csbren  25327  minveclem2  25354  uniioombllem5  25516  itg1mulc  25633  mbfi1fseqlem5  25648  itgconst  25748  itgmulc2  25763  dvexp  25885  dvply1  26219  elqaalem3  26257  aalioulem1  26268  aaliou3lem2  26279  dvtaylp  26306  dvradcnv  26358  pserdvlem2  26366  tangtx  26442  tanregt0  26476  tanarg  26556  logcnlem4  26582  cxpmul  26625  dvcxp1  26677  dvcncxp1  26680  root1eq1  26693  heron  26776  quad2  26777  dcubic1lem  26781  dcubic1  26783  cubic2  26786  binom4  26788  dquartlem1  26789  dquartlem2  26790  dquart  26791  quart1lem  26793  quart1  26794  quartlem1  26795  efiasin  26826  asinsinlem  26829  asinsin  26830  efiatan  26850  efiatan2  26855  2efiatan  26856  atantan  26861  atanbndlem  26863  atans2  26869  atantayl  26875  log2cnv  26882  log2tlbnd  26883  ftalem1  27011  ftalem5  27015  basellem3  27021  basellem5  27023  basellem8  27026  chtub  27151  perfectlem1  27168  perfectlem2  27169  perfect  27170  bcmono  27216  bclbnd  27219  bposlem9  27231  lgsneg  27260  gausslemma2dlem6  27311  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem3  27316  lgseisenlem4  27317  lgsquad2lem1  27323  lgsquad3  27326  2lgslem3a  27335  2lgslem3b  27336  2lgslem3c  27337  2lgslem3d  27338  2lgsoddprmlem2  27348  2sqlem3  27359  chto1ub  27415  rplogsumlem1  27423  dchrmusum2  27433  dchrvmasum2lem  27435  dchrvmasumlem2  27437  dchrvmasumiflem2  27441  dchrisum0lem1  27455  dchrisum0lem2  27457  mulog2sumlem2  27474  chpdifbndlem1  27492  selberg3lem1  27496  selberg4lem1  27499  selberg34r  27510  pntrlog2bndlem3  27518  pntrlog2bndlem5  27520  pntrlog2bndlem6  27522  pntlemh  27538  pntlemr  27541  pntlemf  27544  pntlemk  27545  pntlemo  27546  colinearalglem4  28889  axpasch  28921  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem8  28951  ipasslem4  30816  minvecolem2  30857  his35  31070  leopnmid  32120  quad3d  32737  zringfrac  33526  ccfldsrarelvec  33705  constrrtll  33765  constrrtlc1  33766  constrrtcclem  33768  constrrtcc  33769  cos9thpiminplylem2  33817  oddpwdc  34388  prodfzo03  34637  itgexpif  34640  breprexplemc  34666  circlemeth  34674  hgt750lemg  34688  hgt750lemb  34690  hgt750leme  34692  subfacval2  35252  subfaclim  35253  circum  35739  faclimlem1  35808  faclimlem3  35810  faclim2  35813  unbdqndv2lem1  36574  knoppndvlem2  36578  knoppndvlem7  36583  knoppndvlem11  36587  knoppndvlem12  36588  knoppndvlem14  36590  knoppndvlem18  36594  itgmulc2nc  37748  areacirclem1  37768  areacirclem4  37771  bfplem1  37882  lcmineqlem1  42142  lcmineqlem5  42146  lcmineqlem10  42151  lcmineqlem12  42153  lcmineqlem18  42159  lcmineqlem20  42161  dvrelogpow2b  42181  aks4d1p1p7  42187  primrootscoprmpow  42212  2np3bcnp1  42257  remulcan2d  42375  remul02  42523  remul01  42525  sn-it0e0  42534  remulinvcom  42551  remullid  42552  sn-mullid  42554  remulcand  42557  rediveud  42561  sn-0tie0  42569  sn-mul02  42570  mulgt0b1d  42590  mulgt0b2d  42596  mullt0b1d  42601  sn-itrere  42606  sn-retire  42607  flt4lem5e  42774  flt4lem5f  42775  fltnlta  42781  cu3addd  42798  3cubeslem2  42802  3cubeslem3l  42803  3cubeslem3r  42804  pellexlem6  42951  rmxluc  43053  rmyluc2  43055  rmydbl  43057  jm2.18  43105  jm2.23  43113  jm2.27c  43124  jm3.1lem2  43135  proot1ex  43313  sqrtcval  43758  sqrtcval2  43759  int-mulassocd  44294  binomcxplemnotnn0  44473  mul13d  45405  fmul01lt1lem1  45708  fmul01lt1lem2  45709  coskpi2  45988  cosknegpi  45991  dvnxpaek  46064  dvmptfprodlem  46066  dvnprodlem2  46069  itgsinexplem1  46076  stoweidlem26  46148  wallispilem5  46191  wallispi  46192  wallispi2lem1  46193  wallispi2lem2  46194  stirlinglem3  46198  stirlinglem10  46205  stirlinglem15  46210  dirkertrigeqlem1  46220  dirkertrigeqlem2  46221  dirkertrigeqlem3  46222  dirkertrigeq  46223  dirkercncflem2  46226  fourierdlem66  46294  fourierswlem  46352  fouriersw  46353  etransclem23  46379  etransclem25  46381  etransclem46  46402  hoidmvlelem2  46718  sigarls  46979  sharhght  46987  modmkpkne  47485  fmtnorec4  47673  fmtnoprmfac2lem1  47690  fmtnoprmfac2  47691  fmtnofac2lem  47692  fmtnofac1  47694  lighneallem4a  47732  perfectALTVlem1  47845  perfectALTVlem2  47846  perfectALTV  47847  2zrngmmgm  48376  altgsumbcALT  48477  nn0sumshdiglemB  48745  affinecomb2  48828  itscnhlc0yqe  48884  itschlc0yqe  48885  itsclc0yqsollem1  48887  itsclc0yqsol  48889  itscnhlc0xyqsol  48890  itsclc0xyqsolr  48894  itsclquadb  48901  aacllem  49926