Theorem mulassd 11166

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  recex  11780  mulcand  11781  receu  11793  divmulasscom  11831  divdivdiv  11854  divmuleq  11858  conjmul  11870  modmul1  13884  moddi  13899  expadd  14064  mulbinom2  14183  binom3  14184  digit1  14197  discr1  14199  discr  14200  faclbnd  14250  faclbnd6  14259  bcm1k  14275  bcp1nk  14277  crre  15074  remullem  15088  amgm2  15330  iseraltlem2  15643  iseraltlem3  15644  binomlem  15792  climcndslem2  15813  pwdif  15831  geo2sum  15836  mertenslem1  15847  clim2prod  15851  fallrisefac  15988  binomfallfaclem2  16003  bpolydiflem  16017  bpoly4  16022  sinadd  16129  tanadd  16132  pwp1fsum  16358  bezoutlem3  16508  dvdsmulgcd  16523  qredeq  16624  pcaddlem  16857  prmpwdvds  16873  ablfacrp  20041  nmoco  24727  cph2ass  25205  cphipval2  25233  csbren  25391  minveclem2  25418  uniioombllem5  25579  itg1mulc  25696  mbfi1fseqlem5  25711  itgconst  25811  itgmulc2  25826  dvexp  25945  dvply1  26275  elqaalem3  26312  aalioulem1  26323  aaliou3lem2  26334  dvtaylp  26360  dvradcnv  26411  pserdvlem2  26418  tangtx  26494  tanregt0  26528  tanarg  26608  logcnlem4  26634  cxpmul  26677  dvcxp1  26729  dvcncxp1  26732  root1eq1  26744  heron  26827  quad2  26828  dcubic1lem  26832  dcubic1  26834  cubic2  26837  binom4  26839  dquartlem1  26840  dquartlem2  26841  dquart  26842  quart1lem  26844  quart1  26845  quartlem1  26846  efiasin  26877  asinsinlem  26880  asinsin  26881  efiatan  26901  efiatan2  26906  2efiatan  26907  atantan  26912  atanbndlem  26914  atans2  26920  atantayl  26926  log2cnv  26933  log2tlbnd  26934  ftalem1  27061  ftalem5  27065  basellem3  27071  basellem5  27073  basellem8  27076  chtub  27200  perfectlem1  27217  perfectlem2  27218  perfect  27219  bcmono  27265  bclbnd  27268  bposlem9  27280  lgsneg  27309  gausslemma2dlem6  27360  lgseisenlem1  27363  lgseisenlem2  27364  lgseisenlem3  27365  lgseisenlem4  27366  lgsquad2lem1  27372  lgsquad3  27375  2lgslem3a  27384  2lgslem3b  27385  2lgslem3c  27386  2lgslem3d  27387  2lgsoddprmlem2  27397  2sqlem3  27408  chto1ub  27464  rplogsumlem1  27472  dchrmusum2  27482  dchrvmasum2lem  27484  dchrvmasumlem2  27486  dchrvmasumiflem2  27490  dchrisum0lem1  27504  dchrisum0lem2  27506  mulog2sumlem2  27523  chpdifbndlem1  27541  selberg3lem1  27545  selberg4lem1  27548  selberg34r  27559  pntrlog2bndlem3  27567  pntrlog2bndlem5  27569  pntrlog2bndlem6  27571  pntlemh  27587  pntlemr  27590  pntlemf  27593  pntlemk  27594  pntlemo  27595  colinearalglem4  29003  axpasch  29035  axcontlem2  29059  axcontlem4  29061  axcontlem7  29064  axcontlem8  29065  ipasslem4  30930  minvecolem2  30971  his35  31184  leopnmid  32234  quad3d  32848  zringfrac  33644  ccfldsrarelvec  33862  constrrtll  33922  constrrtlc1  33923  constrrtcclem  33925  constrrtcc  33926  cos9thpiminplylem2  33974  oddpwdc  34545  prodfzo03  34794  itgexpif  34797  breprexplemc  34823  circlemeth  34831  hgt750lemg  34845  hgt750lemb  34847  hgt750leme  34849  subfacval2  35422  subfaclim  35423  circum  35909  faclimlem1  35978  faclimlem3  35980  faclim2  35983  unbdqndv2lem1  36822  knoppndvlem2  36826  knoppndvlem7  36831  knoppndvlem11  36835  knoppndvlem12  36836  knoppndvlem14  36838  knoppndvlem18  36842  itgmulc2nc  38062  areacirclem1  38082  areacirclem4  38085  bfplem1  38196  lcmineqlem1  42521  lcmineqlem5  42525  lcmineqlem10  42530  lcmineqlem12  42532  lcmineqlem18  42538  lcmineqlem20  42540  dvrelogpow2b  42560  aks4d1p1p7  42566  primrootscoprmpow  42591  2np3bcnp1  42636  remulcan2d  42747  remul02  42889  remul01  42891  sn-it0e0  42900  remulinvcom  42917  remullid  42918  sn-mullid  42920  remulcand  42923  rediveud  42927  redivrec2d  42944  rediv23d  42945  sn-0tie0  42948  sn-mul02  42949  mulgt0b1d  42969  mulgt0b2d  42975  mullt0b1d  42980  sn-itrere  42985  sn-retire  42986  flt4lem5e  43113  flt4lem5f  43114  fltnlta  43120  cu3addd  43137  3cubeslem2  43141  3cubeslem3l  43142  3cubeslem3r  43143  pellexlem6  43286  rmxluc  43388  rmyluc2  43390  rmydbl  43392  jm2.18  43440  jm2.23  43448  jm2.27c  43459  jm3.1lem2  43470  proot1ex  43648  sqrtcval  44092  sqrtcval2  44093  int-mulassocd  44628  binomcxplemnotnn0  44807  mul13d  45735  fmul01lt1lem1  46036  fmul01lt1lem2  46037  coskpi2  46316  cosknegpi  46319  dvnxpaek  46392  dvmptfprodlem  46394  dvnprodlem2  46397  itgsinexplem1  46404  stoweidlem26  46476  wallispilem5  46519  wallispi  46520  wallispi2lem1  46521  wallispi2lem2  46522  stirlinglem3  46526  stirlinglem10  46533  stirlinglem15  46538  dirkertrigeqlem1  46548  dirkertrigeqlem2  46549  dirkertrigeqlem3  46550  dirkertrigeq  46551  dirkercncflem2  46554  fourierdlem66  46622  fourierswlem  46680  fouriersw  46681  etransclem23  46707  etransclem25  46709  etransclem46  46730  hoidmvlelem2  47046  sigarls  47307  sharhght  47315  sin3t  47341  cos3t  47342  sin5tlem2  47344  sin5tlem3  47345  sin5tlem4  47346  modmkpkne  47837  fmtnorec4  48034  fmtnoprmfac2lem1  48051  fmtnoprmfac2  48052  fmtnofac2lem  48053  fmtnofac1  48055  lighneallem4a  48093  perfectALTVlem1  48219  perfectALTVlem2  48220  perfectALTV  48221  2zrngmmgm  48750  altgsumbcALT  48851  nn0sumshdiglemB  49118  affinecomb2  49201  itscnhlc0yqe  49257  itschlc0yqe  49258  itsclc0yqsollem1  49260  itsclc0yqsol  49262  itscnhlc0xyqsol  49263  itsclc0xyqsolr  49267  itsclquadb  49274  aacllem  50298