Theorem mulassd 10742

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7170  ℂcc 10613   · cmul 10620

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1090

This theorem is referenced by:  recex  11350  mulcand  11351  receu  11363  divmulasscom  11400  divdivdiv  11419  divmuleq  11423  conjmul  11435  modmul1  13383  moddi  13398  expadd  13563  mulbinom2  13676  binom3  13677  digit1  13690  discr1  13692  discr  13693  faclbnd  13742  faclbnd6  13751  bcm1k  13767  bcp1nk  13769  crre  14563  remullem  14577  amgm2  14819  iseraltlem2  15132  iseraltlem3  15133  binomlem  15277  climcndslem2  15298  pwdif  15316  geo2sum  15321  mertenslem1  15332  clim2prod  15336  fallrisefac  15471  binomfallfaclem2  15486  bpolydiflem  15500  bpoly4  15505  sinadd  15609  tanadd  15612  pwp1fsum  15836  bezoutlem3  15985  dvdsmulgcd  16001  qredeq  16098  pcaddlem  16324  prmpwdvds  16340  ablfacrp  19307  nmoco  23490  cph2ass  23965  cphipval2  23993  csbren  24151  minveclem2  24178  uniioombllem5  24339  itg1mulc  24457  mbfi1fseqlem5  24472  itgconst  24571  itgmulc2  24586  dvexp  24705  dvply1  25032  elqaalem3  25069  aalioulem1  25080  aaliou3lem2  25091  dvtaylp  25117  dvradcnv  25168  pserdvlem2  25175  tangtx  25250  tanregt0  25283  tanarg  25362  logcnlem4  25388  cxpmul  25431  dvcxp1  25481  dvcncxp1  25484  root1eq1  25496  heron  25576  quad2  25577  dcubic1lem  25581  dcubic1  25583  cubic2  25586  binom4  25588  dquartlem1  25589  dquartlem2  25590  dquart  25591  quart1lem  25593  quart1  25594  quartlem1  25595  efiasin  25626  asinsinlem  25629  asinsin  25630  efiatan  25650  efiatan2  25655  2efiatan  25656  atantan  25661  atanbndlem  25663  atans2  25669  atantayl  25675  log2cnv  25682  log2tlbnd  25683  ftalem1  25810  ftalem5  25814  basellem3  25820  basellem5  25822  basellem8  25825  chtub  25948  perfectlem1  25965  perfectlem2  25966  perfect  25967  bcmono  26013  bclbnd  26016  bposlem9  26028  lgsneg  26057  gausslemma2dlem6  26108  lgseisenlem1  26111  lgseisenlem2  26112  lgseisenlem3  26113  lgseisenlem4  26114  lgsquad2lem1  26120  lgsquad3  26123  2lgslem3a  26132  2lgslem3b  26133  2lgslem3c  26134  2lgslem3d  26135  2lgsoddprmlem2  26145  2sqlem3  26156  chto1ub  26212  rplogsumlem1  26220  dchrmusum2  26230  dchrvmasum2lem  26232  dchrvmasumlem2  26234  dchrvmasumiflem2  26238  dchrisum0lem1  26252  dchrisum0lem2  26254  mulog2sumlem2  26271  chpdifbndlem1  26289  selberg3lem1  26293  selberg4lem1  26296  selberg34r  26307  pntrlog2bndlem3  26315  pntrlog2bndlem5  26317  pntrlog2bndlem6  26319  pntlemh  26335  pntlemr  26338  pntlemf  26341  pntlemk  26342  pntlemo  26343  colinearalglem4  26855  axpasch  26887  axcontlem2  26911  axcontlem4  26913  axcontlem7  26916  axcontlem8  26917  ipasslem4  28769  minvecolem2  28810  his35  29023  leopnmid  30073  ccfldsrarelvec  31313  oddpwdc  31891  prodfzo03  32153  itgexpif  32156  breprexplemc  32182  circlemeth  32190  hgt750lemg  32204  hgt750lemb  32206  hgt750leme  32208  subfacval2  32720  subfaclim  32721  circum  33203  faclimlem1  33280  faclimlem3  33282  faclim2  33285  unbdqndv2lem1  34327  knoppndvlem2  34331  knoppndvlem7  34336  knoppndvlem11  34340  knoppndvlem12  34341  knoppndvlem14  34343  knoppndvlem18  34347  itgmulc2nc  35468  areacirclem1  35488  areacirclem4  35491  bfplem1  35603  lcmineqlem1  39657  lcmineqlem5  39661  lcmineqlem10  39666  lcmineqlem12  39668  lcmineqlem18  39674  lcmineqlem20  39676  dvrelogpow2b  39695  aks4d1p1p7  39701  2np3bcnp1  39706  remulcan2d  39869  remul02  39965  remul01  39967  sn-it0e0  39974  remulinvcom  39991  remulid2  39992  sn-mulid2  39994  remulcand  39997  sn-0tie0  39998  sn-mul02  39999  mulgt0b2d  40007  itrere  40013  retire  40014  flt4lem5e  40065  flt4lem5f  40066  fltnlta  40072  cu3addd  40074  3cubeslem2  40079  3cubeslem3l  40080  3cubeslem3r  40081  pellexlem6  40228  rmxluc  40330  rmyluc2  40332  rmydbl  40334  jm2.18  40382  jm2.23  40390  jm2.27c  40401  jm3.1lem2  40412  proot1ex  40598  sqrtcval  40794  sqrtcval2  40795  int-mulassocd  41335  binomcxplemnotnn0  41512  mul13d  42355  fmul01lt1lem1  42667  fmul01lt1lem2  42668  coskpi2  42949  cosknegpi  42952  dvnxpaek  43025  dvmptfprodlem  43027  dvnprodlem2  43030  itgsinexplem1  43037  stoweidlem26  43109  wallispilem5  43152  wallispi  43153  wallispi2lem1  43154  wallispi2lem2  43155  stirlinglem3  43159  stirlinglem10  43166  stirlinglem15  43171  dirkertrigeqlem1  43181  dirkertrigeqlem2  43182  dirkertrigeqlem3  43183  dirkertrigeq  43184  dirkercncflem2  43187  fourierdlem66  43255  fourierswlem  43313  fouriersw  43314  etransclem23  43340  etransclem25  43342  etransclem46  43363  hoidmvlelem2  43676  sigarls  43912  sharhght  43920  fmtnorec4  44535  fmtnoprmfac2lem1  44552  fmtnoprmfac2  44553  fmtnofac2lem  44554  fmtnofac1  44556  lighneallem4a  44594  perfectALTVlem1  44707  perfectALTVlem2  44708  perfectALTV  44709  2zrngmmgm  45038  altgsumbcALT  45223  nn0sumshdiglemB  45500  affinecomb2  45583  itscnhlc0yqe  45639  itschlc0yqe  45640  itsclc0yqsollem1  45642  itsclc0yqsol  45644  itscnhlc0xyqsol  45645  itsclc0xyqsolr  45649  itsclquadb  45656  aacllem  45958