Theorem mulassd 11251

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7400  ℂcc 11120   · cmul 11127

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

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

This theorem is referenced by:  recex  11862  mulcand  11863  receu  11875  divmulasscom  11913  divdivdiv  11935  divmuleq  11939  conjmul  11951  modmul1  13932  moddi  13947  expadd  14112  mulbinom2  14231  binom3  14232  digit1  14245  discr1  14247  discr  14248  faclbnd  14298  faclbnd6  14307  bcm1k  14323  bcp1nk  14325  crre  15122  remullem  15136  amgm2  15377  iseraltlem2  15688  iseraltlem3  15689  binomlem  15834  climcndslem2  15855  pwdif  15873  geo2sum  15878  mertenslem1  15889  clim2prod  15893  fallrisefac  16030  binomfallfaclem2  16045  bpolydiflem  16059  bpoly4  16064  sinadd  16169  tanadd  16172  pwp1fsum  16397  bezoutlem3  16547  dvdsmulgcd  16562  qredeq  16663  pcaddlem  16895  prmpwdvds  16911  ablfacrp  20036  nmoco  24663  cph2ass  25152  cphipval2  25180  csbren  25338  minveclem2  25365  uniioombllem5  25527  itg1mulc  25644  mbfi1fseqlem5  25659  itgconst  25759  itgmulc2  25774  dvexp  25896  dvply1  26230  elqaalem3  26268  aalioulem1  26279  aaliou3lem2  26290  dvtaylp  26317  dvradcnv  26369  pserdvlem2  26377  tangtx  26452  tanregt0  26486  tanarg  26566  logcnlem4  26592  cxpmul  26635  dvcxp1  26687  dvcncxp1  26690  root1eq1  26703  heron  26786  quad2  26787  dcubic1lem  26791  dcubic1  26793  cubic2  26796  binom4  26798  dquartlem1  26799  dquartlem2  26800  dquart  26801  quart1lem  26803  quart1  26804  quartlem1  26805  efiasin  26836  asinsinlem  26839  asinsin  26840  efiatan  26860  efiatan2  26865  2efiatan  26866  atantan  26871  atanbndlem  26873  atans2  26879  atantayl  26885  log2cnv  26892  log2tlbnd  26893  ftalem1  27021  ftalem5  27025  basellem3  27031  basellem5  27033  basellem8  27036  chtub  27161  perfectlem1  27178  perfectlem2  27179  perfect  27180  bcmono  27226  bclbnd  27229  bposlem9  27241  lgsneg  27270  gausslemma2dlem6  27321  lgseisenlem1  27324  lgseisenlem2  27325  lgseisenlem3  27326  lgseisenlem4  27327  lgsquad2lem1  27333  lgsquad3  27336  2lgslem3a  27345  2lgslem3b  27346  2lgslem3c  27347  2lgslem3d  27348  2lgsoddprmlem2  27358  2sqlem3  27369  chto1ub  27425  rplogsumlem1  27433  dchrmusum2  27443  dchrvmasum2lem  27445  dchrvmasumlem2  27447  dchrvmasumiflem2  27451  dchrisum0lem1  27465  dchrisum0lem2  27467  mulog2sumlem2  27484  chpdifbndlem1  27502  selberg3lem1  27506  selberg4lem1  27509  selberg34r  27520  pntrlog2bndlem3  27528  pntrlog2bndlem5  27530  pntrlog2bndlem6  27532  pntlemh  27548  pntlemr  27551  pntlemf  27554  pntlemk  27555  pntlemo  27556  colinearalglem4  28822  axpasch  28854  axcontlem2  28878  axcontlem4  28880  axcontlem7  28883  axcontlem8  28884  ipasslem4  30749  minvecolem2  30790  his35  31003  leopnmid  32053  quad3d  32663  zringfrac  33506  ccfldsrarelvec  33647  constrrtll  33700  constrrtlc1  33701  constrrtcclem  33703  constrrtcc  33704  cos9thpiminplylem2  33752  oddpwdc  34315  prodfzo03  34564  itgexpif  34567  breprexplemc  34593  circlemeth  34601  hgt750lemg  34615  hgt750lemb  34617  hgt750leme  34619  subfacval2  35138  subfaclim  35139  circum  35625  faclimlem1  35689  faclimlem3  35691  faclim2  35694  unbdqndv2lem1  36456  knoppndvlem2  36460  knoppndvlem7  36465  knoppndvlem11  36469  knoppndvlem12  36470  knoppndvlem14  36472  knoppndvlem18  36476  itgmulc2nc  37641  areacirclem1  37661  areacirclem4  37664  bfplem1  37775  lcmineqlem1  41971  lcmineqlem5  41975  lcmineqlem10  41980  lcmineqlem12  41982  lcmineqlem18  41988  lcmineqlem20  41990  dvrelogpow2b  42010  aks4d1p1p7  42016  primrootscoprmpow  42041  2np3bcnp1  42086  remulcan2d  42238  remul02  42380  remul01  42382  sn-it0e0  42390  remulinvcom  42407  remullid  42408  sn-mullid  42410  remulcand  42413  sn-0tie0  42414  sn-mul02  42415  mulgt0b2d  42435  sn-itrere  42443  sn-retire  42444  flt4lem5e  42611  flt4lem5f  42612  fltnlta  42618  cu3addd  42636  3cubeslem2  42640  3cubeslem3l  42641  3cubeslem3r  42642  pellexlem6  42789  rmxluc  42892  rmyluc2  42894  rmydbl  42896  jm2.18  42944  jm2.23  42952  jm2.27c  42963  jm3.1lem2  42974  proot1ex  43152  sqrtcval  43597  sqrtcval2  43598  int-mulassocd  44133  binomcxplemnotnn0  44313  mul13d  45242  fmul01lt1lem1  45549  fmul01lt1lem2  45550  coskpi2  45831  cosknegpi  45834  dvnxpaek  45907  dvmptfprodlem  45909  dvnprodlem2  45912  itgsinexplem1  45919  stoweidlem26  45991  wallispilem5  46034  wallispi  46035  wallispi2lem1  46036  wallispi2lem2  46037  stirlinglem3  46041  stirlinglem10  46048  stirlinglem15  46053  dirkertrigeqlem1  46063  dirkertrigeqlem2  46064  dirkertrigeqlem3  46065  dirkertrigeq  46066  dirkercncflem2  46069  fourierdlem66  46137  fourierswlem  46195  fouriersw  46196  etransclem23  46222  etransclem25  46224  etransclem46  46245  hoidmvlelem2  46561  sigarls  46822  sharhght  46830  fmtnorec4  47489  fmtnoprmfac2lem1  47506  fmtnoprmfac2  47507  fmtnofac2lem  47508  fmtnofac1  47510  lighneallem4a  47548  perfectALTVlem1  47661  perfectALTVlem2  47662  perfectALTV  47663  2zrngmmgm  48121  altgsumbcALT  48222  nn0sumshdiglemB  48494  affinecomb2  48577  itscnhlc0yqe  48633  itschlc0yqe  48634  itsclc0yqsollem1  48636  itsclc0yqsol  48638  itscnhlc0xyqsol  48639  itsclc0xyqsolr  48643  itsclquadb  48650  aacllem  49506