Theorem mulassd 10929

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  recex  11537  mulcand  11538  receu  11550  divmulasscom  11587  divdivdiv  11606  divmuleq  11610  conjmul  11622  modmul1  13572  moddi  13587  expadd  13753  mulbinom2  13866  binom3  13867  digit1  13880  discr1  13882  discr  13883  faclbnd  13932  faclbnd6  13941  bcm1k  13957  bcp1nk  13959  crre  14753  remullem  14767  amgm2  15009  iseraltlem2  15322  iseraltlem3  15323  binomlem  15469  climcndslem2  15490  pwdif  15508  geo2sum  15513  mertenslem1  15524  clim2prod  15528  fallrisefac  15663  binomfallfaclem2  15678  bpolydiflem  15692  bpoly4  15697  sinadd  15801  tanadd  15804  pwp1fsum  16028  bezoutlem3  16177  dvdsmulgcd  16193  qredeq  16290  pcaddlem  16517  prmpwdvds  16533  ablfacrp  19584  nmoco  23807  cph2ass  24282  cphipval2  24310  csbren  24468  minveclem2  24495  uniioombllem5  24656  itg1mulc  24774  mbfi1fseqlem5  24789  itgconst  24888  itgmulc2  24903  dvexp  25022  dvply1  25349  elqaalem3  25386  aalioulem1  25397  aaliou3lem2  25408  dvtaylp  25434  dvradcnv  25485  pserdvlem2  25492  tangtx  25567  tanregt0  25600  tanarg  25679  logcnlem4  25705  cxpmul  25748  dvcxp1  25798  dvcncxp1  25801  root1eq1  25813  heron  25893  quad2  25894  dcubic1lem  25898  dcubic1  25900  cubic2  25903  binom4  25905  dquartlem1  25906  dquartlem2  25907  dquart  25908  quart1lem  25910  quart1  25911  quartlem1  25912  efiasin  25943  asinsinlem  25946  asinsin  25947  efiatan  25967  efiatan2  25972  2efiatan  25973  atantan  25978  atanbndlem  25980  atans2  25986  atantayl  25992  log2cnv  25999  log2tlbnd  26000  ftalem1  26127  ftalem5  26131  basellem3  26137  basellem5  26139  basellem8  26142  chtub  26265  perfectlem1  26282  perfectlem2  26283  perfect  26284  bcmono  26330  bclbnd  26333  bposlem9  26345  lgsneg  26374  gausslemma2dlem6  26425  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgsquad2lem1  26437  lgsquad3  26440  2lgslem3a  26449  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2lgsoddprmlem2  26462  2sqlem3  26473  chto1ub  26529  rplogsumlem1  26537  dchrmusum2  26547  dchrvmasum2lem  26549  dchrvmasumlem2  26551  dchrvmasumiflem2  26555  dchrisum0lem1  26569  dchrisum0lem2  26571  mulog2sumlem2  26588  chpdifbndlem1  26606  selberg3lem1  26610  selberg4lem1  26613  selberg34r  26624  pntrlog2bndlem3  26632  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntlemh  26652  pntlemr  26655  pntlemf  26658  pntlemk  26659  pntlemo  26660  colinearalglem4  27180  axpasch  27212  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  ipasslem4  29097  minvecolem2  29138  his35  29351  leopnmid  30401  ccfldsrarelvec  31643  oddpwdc  32221  prodfzo03  32483  itgexpif  32486  breprexplemc  32512  circlemeth  32520  hgt750lemg  32534  hgt750lemb  32536  hgt750leme  32538  subfacval2  33049  subfaclim  33050  circum  33532  faclimlem1  33615  faclimlem3  33617  faclim2  33620  unbdqndv2lem1  34616  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem11  34629  knoppndvlem12  34630  knoppndvlem14  34632  knoppndvlem18  34636  itgmulc2nc  35772  areacirclem1  35792  areacirclem4  35795  bfplem1  35907  lcmineqlem1  39965  lcmineqlem5  39969  lcmineqlem10  39974  lcmineqlem12  39976  lcmineqlem18  39982  lcmineqlem20  39984  dvrelogpow2b  40004  aks4d1p1p7  40010  2np3bcnp1  40028  remulcan2d  40214  remul02  40309  remul01  40311  sn-it0e0  40318  remulinvcom  40335  remulid2  40336  sn-mulid2  40338  remulcand  40341  sn-0tie0  40342  sn-mul02  40343  mulgt0b2d  40351  itrere  40357  retire  40358  flt4lem5e  40409  flt4lem5f  40410  fltnlta  40416  cu3addd  40418  3cubeslem2  40423  3cubeslem3l  40424  3cubeslem3r  40425  pellexlem6  40572  rmxluc  40674  rmyluc2  40676  rmydbl  40678  jm2.18  40726  jm2.23  40734  jm2.27c  40745  jm3.1lem2  40756  proot1ex  40942  sqrtcval  41138  sqrtcval2  41139  int-mulassocd  41677  binomcxplemnotnn0  41863  mul13d  42707  fmul01lt1lem1  43015  fmul01lt1lem2  43016  coskpi2  43297  cosknegpi  43300  dvnxpaek  43373  dvmptfprodlem  43375  dvnprodlem2  43378  itgsinexplem1  43385  stoweidlem26  43457  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  stirlinglem3  43507  stirlinglem10  43514  stirlinglem15  43519  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem2  43535  fourierdlem66  43603  fourierswlem  43661  fouriersw  43662  etransclem23  43688  etransclem25  43690  etransclem46  43711  hoidmvlelem2  44024  sigarls  44260  sharhght  44268  fmtnorec4  44889  fmtnoprmfac2lem1  44906  fmtnoprmfac2  44907  fmtnofac2lem  44908  fmtnofac1  44910  lighneallem4a  44948  perfectALTVlem1  45061  perfectALTVlem2  45062  perfectALTV  45063  2zrngmmgm  45392  altgsumbcALT  45577  nn0sumshdiglemB  45854  affinecomb2  45937  itscnhlc0yqe  45993  itschlc0yqe  45994  itsclc0yqsollem1  45996  itsclc0yqsol  45998  itscnhlc0xyqsol  45999  itsclc0xyqsolr  46003  itsclquadb  46010  aacllem  46391