Theorem mulassd 11268

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11137   · cmul 11144

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

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

This theorem is referenced by:  recex  11877  mulcand  11878  receu  11890  divmulasscom  11927  divdivdiv  11946  divmuleq  11950  conjmul  11962  modmul1  13922  moddi  13937  expadd  14102  mulbinom2  14218  binom3  14219  digit1  14232  discr1  14234  discr  14235  faclbnd  14282  faclbnd6  14291  bcm1k  14307  bcp1nk  14309  crre  15094  remullem  15108  amgm2  15349  iseraltlem2  15662  iseraltlem3  15663  binomlem  15808  climcndslem2  15829  pwdif  15847  geo2sum  15852  mertenslem1  15863  clim2prod  15867  fallrisefac  16002  binomfallfaclem2  16017  bpolydiflem  16031  bpoly4  16036  sinadd  16141  tanadd  16144  pwp1fsum  16368  bezoutlem3  16517  dvdsmulgcd  16531  qredeq  16628  pcaddlem  16857  prmpwdvds  16873  ablfacrp  20023  nmoco  24667  cph2ass  25154  cphipval2  25182  csbren  25340  minveclem2  25367  uniioombllem5  25529  itg1mulc  25647  mbfi1fseqlem5  25662  itgconst  25761  itgmulc2  25776  dvexp  25898  dvply1  26231  elqaalem3  26269  aalioulem1  26280  aaliou3lem2  26291  dvtaylp  26318  dvradcnv  26370  pserdvlem2  26378  tangtx  26453  tanregt0  26486  tanarg  26566  logcnlem4  26592  cxpmul  26635  dvcxp1  26687  dvcncxp1  26690  root1eq1  26703  heron  26783  quad2  26784  dcubic1lem  26788  dcubic1  26790  cubic2  26793  binom4  26795  dquartlem1  26796  dquartlem2  26797  dquart  26798  quart1lem  26800  quart1  26801  quartlem1  26802  efiasin  26833  asinsinlem  26836  asinsin  26837  efiatan  26857  efiatan2  26862  2efiatan  26863  atantan  26868  atanbndlem  26870  atans2  26876  atantayl  26882  log2cnv  26889  log2tlbnd  26890  ftalem1  27018  ftalem5  27022  basellem3  27028  basellem5  27030  basellem8  27033  chtub  27158  perfectlem1  27175  perfectlem2  27176  perfect  27177  bcmono  27223  bclbnd  27226  bposlem9  27238  lgsneg  27267  gausslemma2dlem6  27318  lgseisenlem1  27321  lgseisenlem2  27322  lgseisenlem3  27323  lgseisenlem4  27324  lgsquad2lem1  27330  lgsquad3  27333  2lgslem3a  27342  2lgslem3b  27343  2lgslem3c  27344  2lgslem3d  27345  2lgsoddprmlem2  27355  2sqlem3  27366  chto1ub  27422  rplogsumlem1  27430  dchrmusum2  27440  dchrvmasum2lem  27442  dchrvmasumlem2  27444  dchrvmasumiflem2  27448  dchrisum0lem1  27462  dchrisum0lem2  27464  mulog2sumlem2  27481  chpdifbndlem1  27499  selberg3lem1  27503  selberg4lem1  27506  selberg34r  27517  pntrlog2bndlem3  27525  pntrlog2bndlem5  27527  pntrlog2bndlem6  27529  pntlemh  27545  pntlemr  27548  pntlemf  27551  pntlemk  27552  pntlemo  27553  colinearalglem4  28733  axpasch  28765  axcontlem2  28789  axcontlem4  28791  axcontlem7  28794  axcontlem8  28795  ipasslem4  30657  minvecolem2  30698  his35  30911  leopnmid  31961  zringfrac  33009  ccfldsrarelvec  33359  oddpwdc  33974  prodfzo03  34235  itgexpif  34238  breprexplemc  34264  circlemeth  34272  hgt750lemg  34286  hgt750lemb  34288  hgt750leme  34290  subfacval2  34797  subfaclim  34798  circum  35278  faclimlem1  35337  faclimlem3  35339  faclim2  35342  unbdqndv2lem1  35984  knoppndvlem2  35988  knoppndvlem7  35993  knoppndvlem11  35997  knoppndvlem12  35998  knoppndvlem14  36000  knoppndvlem18  36004  itgmulc2nc  37161  areacirclem1  37181  areacirclem4  37184  bfplem1  37295  lcmineqlem1  41500  lcmineqlem5  41504  lcmineqlem10  41509  lcmineqlem12  41511  lcmineqlem18  41517  lcmineqlem20  41519  dvrelogpow2b  41539  aks4d1p1p7  41545  primrootscoprmpow  41570  2np3bcnp1  41616  remulcan2d  41838  remul02  41960  remul01  41962  sn-it0e0  41970  remulinvcom  41987  remullid  41988  sn-mullid  41990  remulcand  41993  sn-0tie0  41994  sn-mul02  41995  mulgt0b2d  42015  sn-itrere  42021  sn-retire  42022  flt4lem5e  42080  flt4lem5f  42081  fltnlta  42087  cu3addd  42100  3cubeslem2  42105  3cubeslem3l  42106  3cubeslem3r  42107  pellexlem6  42254  rmxluc  42357  rmyluc2  42359  rmydbl  42361  jm2.18  42409  jm2.23  42417  jm2.27c  42428  jm3.1lem2  42439  proot1ex  42624  sqrtcval  43071  sqrtcval2  43072  int-mulassocd  43607  binomcxplemnotnn0  43793  mul13d  44661  fmul01lt1lem1  44972  fmul01lt1lem2  44973  coskpi2  45254  cosknegpi  45257  dvnxpaek  45330  dvmptfprodlem  45332  dvnprodlem2  45335  itgsinexplem1  45342  stoweidlem26  45414  wallispilem5  45457  wallispi  45458  wallispi2lem1  45459  wallispi2lem2  45460  stirlinglem3  45464  stirlinglem10  45471  stirlinglem15  45476  dirkertrigeqlem1  45486  dirkertrigeqlem2  45487  dirkertrigeqlem3  45488  dirkertrigeq  45489  dirkercncflem2  45492  fourierdlem66  45560  fourierswlem  45618  fouriersw  45619  etransclem23  45645  etransclem25  45647  etransclem46  45668  hoidmvlelem2  45984  sigarls  46245  sharhght  46253  fmtnorec4  46889  fmtnoprmfac2lem1  46906  fmtnoprmfac2  46907  fmtnofac2lem  46908  fmtnofac1  46910  lighneallem4a  46948  perfectALTVlem1  47061  perfectALTVlem2  47062  perfectALTV  47063  2zrngmmgm  47314  altgsumbcALT  47417  nn0sumshdiglemB  47693  affinecomb2  47776  itscnhlc0yqe  47832  itschlc0yqe  47833  itsclc0yqsollem1  47835  itsclc0yqsol  47837  itscnhlc0xyqsol  47838  itsclc0xyqsolr  47842  itsclquadb  47849  aacllem  48234