Theorem mulassd 10666

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   · cmul 10544

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  recex  11274  mulcand  11275  receu  11287  divmulasscom  11324  divdivdiv  11343  divmuleq  11347  conjmul  11359  modmul1  13295  moddi  13310  expadd  13474  mulbinom2  13587  binom3  13588  digit1  13601  discr1  13603  discr  13604  faclbnd  13653  faclbnd6  13662  bcm1k  13678  bcp1nk  13680  crre  14475  remullem  14489  amgm2  14731  iseraltlem2  15041  iseraltlem3  15042  binomlem  15186  climcndslem2  15207  pwdif  15225  geo2sum  15231  mertenslem1  15242  clim2prod  15246  fallrisefac  15381  binomfallfaclem2  15396  bpolydiflem  15410  bpoly4  15415  sinadd  15519  tanadd  15522  pwp1fsum  15744  bezoutlem3  15891  dvdsmulgcd  15907  qredeq  16003  pcaddlem  16226  prmpwdvds  16242  ablfacrp  19190  nmoco  23348  cph2ass  23819  cphipval2  23846  csbren  24004  minveclem2  24031  uniioombllem5  24190  itg1mulc  24307  mbfi1fseqlem5  24322  itgconst  24421  itgmulc2  24436  dvexp  24552  dvply1  24875  elqaalem3  24912  aalioulem1  24923  aaliou3lem2  24934  dvtaylp  24960  dvradcnv  25011  pserdvlem2  25018  tangtx  25093  tanregt0  25125  tanarg  25204  logcnlem4  25230  cxpmul  25273  dvcxp1  25323  dvcncxp1  25326  root1eq1  25338  heron  25418  quad2  25419  dcubic1lem  25423  dcubic1  25425  cubic2  25428  binom4  25430  dquartlem1  25431  dquartlem2  25432  dquart  25433  quart1lem  25435  quart1  25436  quartlem1  25437  efiasin  25468  asinsinlem  25471  asinsin  25472  efiatan  25492  efiatan2  25497  2efiatan  25498  atantan  25503  atanbndlem  25505  atans2  25511  atantayl  25517  log2cnv  25524  log2tlbnd  25525  ftalem1  25652  ftalem5  25656  basellem3  25662  basellem5  25664  basellem8  25667  chtub  25790  perfectlem1  25807  perfectlem2  25808  perfect  25809  bcmono  25855  bclbnd  25858  bposlem9  25870  lgsneg  25899  gausslemma2dlem6  25950  lgseisenlem1  25953  lgseisenlem2  25954  lgseisenlem3  25955  lgseisenlem4  25956  lgsquad2lem1  25962  lgsquad3  25965  2lgslem3a  25974  2lgslem3b  25975  2lgslem3c  25976  2lgslem3d  25977  2lgsoddprmlem2  25987  2sqlem3  25998  chto1ub  26054  rplogsumlem1  26062  dchrmusum2  26072  dchrvmasum2lem  26074  dchrvmasumlem2  26076  dchrvmasumiflem2  26080  dchrisum0lem1  26094  dchrisum0lem2  26096  mulog2sumlem2  26113  chpdifbndlem1  26131  selberg3lem1  26135  selberg4lem1  26138  selberg34r  26149  pntrlog2bndlem3  26157  pntrlog2bndlem5  26159  pntrlog2bndlem6  26161  pntlemh  26177  pntlemr  26180  pntlemf  26183  pntlemk  26184  pntlemo  26185  colinearalglem4  26697  axpasch  26729  axcontlem2  26753  axcontlem4  26755  axcontlem7  26758  axcontlem8  26759  ipasslem4  28613  minvecolem2  28654  his35  28867  leopnmid  29917  ccfldsrarelvec  31058  oddpwdc  31614  prodfzo03  31876  itgexpif  31879  breprexplemc  31905  circlemeth  31913  hgt750lemg  31927  hgt750lemb  31929  hgt750leme  31931  subfacval2  32436  subfaclim  32437  circum  32919  faclimlem1  32977  faclimlem3  32979  faclim2  32982  unbdqndv2lem1  33850  knoppndvlem2  33854  knoppndvlem7  33859  knoppndvlem11  33863  knoppndvlem12  33864  knoppndvlem14  33866  knoppndvlem18  33870  itgmulc2nc  34962  areacirclem1  34984  areacirclem4  34987  bfplem1  35102  remulcan2d  39163  remul02  39242  remul01  39244  remulinvcom  39255  remulid2  39256  remulcand  39257  fltnlta  39282  cu3addd  39284  3cubeslem2  39289  3cubeslem3l  39290  3cubeslem3r  39291  pellexlem6  39438  rmxluc  39540  rmyluc2  39542  rmydbl  39544  jm2.18  39592  jm2.23  39600  jm2.27c  39611  jm3.1lem2  39622  proot1ex  39808  int-mulassocd  40537  binomcxplemnotnn0  40695  mul13d  41552  fmul01lt1lem1  41872  fmul01lt1lem2  41873  coskpi2  42154  cosknegpi  42157  dvnxpaek  42234  dvmptfprodlem  42236  dvnprodlem2  42239  itgsinexplem1  42246  stoweidlem26  42318  wallispilem5  42361  wallispi  42362  wallispi2lem1  42363  wallispi2lem2  42364  stirlinglem3  42368  stirlinglem10  42375  stirlinglem15  42380  dirkertrigeqlem1  42390  dirkertrigeqlem2  42391  dirkertrigeqlem3  42392  dirkertrigeq  42393  dirkercncflem2  42396  fourierdlem66  42464  fourierswlem  42522  fouriersw  42523  etransclem23  42549  etransclem25  42551  etransclem46  42572  hoidmvlelem2  42885  sigarls  43121  sharhght  43129  fmtnorec4  43718  fmtnoprmfac2lem1  43735  fmtnoprmfac2  43736  fmtnofac2lem  43737  fmtnofac1  43739  lighneallem4a  43780  perfectALTVlem1  43893  perfectALTVlem2  43894  perfectALTV  43895  2zrngmmgm  44224  altgsumbcALT  44408  nn0sumshdiglemB  44687  affinecomb2  44697  itscnhlc0yqe  44753  itschlc0yqe  44754  itsclc0yqsollem1  44756  itsclc0yqsol  44758  itscnhlc0xyqsol  44759  itsclc0xyqsolr  44763  itsclquadb  44770  aacllem  44909