MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulassd Structured version   Visualization version   GIF version

Theorem mulassd 10101
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
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addassd.3 . 2 (𝜑𝐶 ∈ ℂ)
4 mulass 10062 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1366 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972   · cmul 9979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10040
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1056
This theorem is referenced by:  recex  10697  mulcand  10698  receu  10710  divmulasscom  10747  divdivdiv  10764  divmuleq  10768  conjmul  10780  modmul1  12763  moddi  12778  expadd  12942  mulbinom2  13024  binom3  13025  digit1  13038  discr1  13040  discr  13041  faclbnd  13117  faclbnd6  13126  bcm1k  13142  bcp1nk  13144  crre  13898  remullem  13912  amgm2  14153  iseraltlem2  14457  iseraltlem3  14458  binomlem  14605  climcndslem2  14626  geo2sum  14648  mertenslem1  14660  clim2prod  14664  fallrisefac  14800  binomfallfaclem2  14815  bpolydiflem  14829  bpoly4  14834  sinadd  14938  tanadd  14941  pwp1fsum  15161  bezoutlem3  15305  dvdsmulgcd  15321  qredeq  15418  pcaddlem  15639  prmpwdvds  15655  ablfacrp  18511  nmoco  22588  cph2ass  23059  cphipval2  23086  csbren  23228  minveclem2  23243  uniioombllem5  23401  itg1mulc  23516  mbfi1fseqlem5  23531  itgconst  23630  itgmulc2  23645  dvexp  23761  dvply1  24084  elqaalem3  24121  aalioulem1  24132  aaliou3lem2  24143  dvtaylp  24169  dvradcnv  24220  pserdvlem2  24227  tangtx  24302  tanregt0  24330  tanarg  24410  logcnlem4  24436  cxpmul  24479  dvcxp1  24526  dvcncxp1  24529  root1eq1  24541  heron  24610  quad2  24611  dcubic1lem  24615  dcubic1  24617  cubic2  24620  binom4  24622  dquartlem1  24623  dquartlem2  24624  dquart  24625  quart1lem  24627  quart1  24628  quartlem1  24629  efiasin  24660  asinsinlem  24663  asinsin  24664  efiatan  24684  efiatan2  24689  2efiatan  24690  atantan  24695  atanbndlem  24697  atans2  24703  atantayl  24709  log2cnv  24716  log2tlbnd  24717  ftalem1  24844  ftalem5  24848  basellem3  24854  basellem5  24856  basellem8  24859  chtub  24982  perfectlem1  24999  perfectlem2  25000  perfect  25001  bcmono  25047  bclbnd  25050  bposlem9  25062  lgsneg  25091  gausslemma2dlem6  25142  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgsquad2lem1  25154  lgsquad3  25157  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  2lgsoddprmlem2  25179  2sqlem3  25190  chto1ub  25210  rplogsumlem1  25218  dchrmusum2  25228  dchrvmasum2lem  25230  dchrvmasumlem2  25232  dchrvmasumiflem2  25236  dchrisum0lem1  25250  dchrisum0lem2  25252  mulog2sumlem2  25269  chpdifbndlem1  25287  selberg3lem1  25291  selberg4lem1  25294  selberg34r  25305  pntrlog2bndlem3  25313  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntlemh  25333  pntlemr  25336  pntlemf  25339  pntlemk  25340  pntlemo  25341  colinearalglem4  25834  axpasch  25866  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  ipasslem4  27817  minvecolem2  27859  his35  28073  leopnmid  29125  oddpwdc  30544  prodfzo03  30809  itgexpif  30812  breprexplemc  30838  circlemeth  30846  hgt750lemg  30860  hgt750lemb  30862  hgt750leme  30864  subfacval2  31295  subfaclim  31296  circum  31694  faclimlem1  31755  faclimlem3  31757  faclim2  31760  unbdqndv2lem1  32625  knoppndvlem2  32629  knoppndvlem7  32634  knoppndvlem11  32638  knoppndvlem12  32639  knoppndvlem14  32641  knoppndvlem18  32645  itgmulc2nc  33608  areacirclem1  33630  areacirclem4  33633  bfplem1  33751  pellexlem6  37715  rmxluc  37818  rmyluc2  37820  rmydbl  37822  jm2.18  37872  jm2.23  37880  jm2.27c  37891  jm3.1lem2  37902  proot1ex  38096  int-mulassocd  38797  binomcxplemnotnn0  38872  mul13d  39805  fmul01lt1lem1  40134  fmul01lt1lem2  40135  coskpi2  40395  cosknegpi  40398  dvnxpaek  40475  dvmptfprodlem  40477  dvnprodlem2  40480  itgsinexplem1  40487  stoweidlem26  40561  wallispilem5  40604  wallispi  40605  wallispi2lem1  40606  wallispi2lem2  40607  stirlinglem3  40611  stirlinglem10  40618  stirlinglem15  40623  dirkertrigeqlem1  40633  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem2  40639  fourierdlem66  40707  fourierswlem  40765  fouriersw  40766  etransclem23  40792  etransclem25  40794  etransclem46  40815  hoidmvlelem2  41131  sigarls  41367  sharhght  41375  fmtnorec4  41786  fmtnoprmfac2lem1  41803  fmtnoprmfac2  41804  fmtnofac2lem  41805  fmtnofac1  41807  pwdif  41826  lighneallem4a  41850  perfectALTVlem1  41955  perfectALTVlem2  41956  perfectALTV  41957  2zrngmmgm  42271  altgsumbcALT  42456  nn0sumshdiglemB  42739  aacllem  42875
  Copyright terms: Public domain W3C validator