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

Theorem mulassd 10656
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 10617 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1365 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  (class class class)co 7148  cc 10527   · cmul 10534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10595
This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1083
This theorem is referenced by:  recex  11264  mulcand  11265  receu  11277  divmulasscom  11314  divdivdiv  11333  divmuleq  11337  conjmul  11349  modmul1  13284  moddi  13299  expadd  13463  mulbinom2  13576  binom3  13577  digit1  13590  discr1  13592  discr  13593  faclbnd  13642  faclbnd6  13651  bcm1k  13667  bcp1nk  13669  crre  14465  remullem  14479  amgm2  14721  iseraltlem2  15031  iseraltlem3  15032  binomlem  15176  climcndslem2  15197  pwdif  15215  geo2sum  15221  mertenslem1  15232  clim2prod  15236  fallrisefac  15371  binomfallfaclem2  15386  bpolydiflem  15400  bpoly4  15405  sinadd  15509  tanadd  15512  pwp1fsum  15734  bezoutlem3  15881  dvdsmulgcd  15897  qredeq  15993  pcaddlem  16216  prmpwdvds  16232  ablfacrp  19180  nmoco  23338  cph2ass  23809  cphipval2  23836  csbren  23994  minveclem2  24021  uniioombllem5  24180  itg1mulc  24297  mbfi1fseqlem5  24312  itgconst  24411  itgmulc2  24426  dvexp  24542  dvply1  24865  elqaalem3  24902  aalioulem1  24913  aaliou3lem2  24924  dvtaylp  24950  dvradcnv  25001  pserdvlem2  25008  tangtx  25083  tanregt0  25115  tanarg  25194  logcnlem4  25220  cxpmul  25263  dvcxp1  25313  dvcncxp1  25316  root1eq1  25328  heron  25408  quad2  25409  dcubic1lem  25413  dcubic1  25415  cubic2  25418  binom4  25420  dquartlem1  25421  dquartlem2  25422  dquart  25423  quart1lem  25425  quart1  25426  quartlem1  25427  efiasin  25458  asinsinlem  25461  asinsin  25462  efiatan  25482  efiatan2  25487  2efiatan  25488  atantan  25493  atanbndlem  25495  atans2  25501  atantayl  25507  log2cnv  25514  log2tlbnd  25515  ftalem1  25642  ftalem5  25646  basellem3  25652  basellem5  25654  basellem8  25657  chtub  25780  perfectlem1  25797  perfectlem2  25798  perfect  25799  bcmono  25845  bclbnd  25848  bposlem9  25860  lgsneg  25889  gausslemma2dlem6  25940  lgseisenlem1  25943  lgseisenlem2  25944  lgseisenlem3  25945  lgseisenlem4  25946  lgsquad2lem1  25952  lgsquad3  25955  2lgslem3a  25964  2lgslem3b  25965  2lgslem3c  25966  2lgslem3d  25967  2lgsoddprmlem2  25977  2sqlem3  25988  chto1ub  26044  rplogsumlem1  26052  dchrmusum2  26062  dchrvmasum2lem  26064  dchrvmasumlem2  26066  dchrvmasumiflem2  26070  dchrisum0lem1  26084  dchrisum0lem2  26086  mulog2sumlem2  26103  chpdifbndlem1  26121  selberg3lem1  26125  selberg4lem1  26128  selberg34r  26139  pntrlog2bndlem3  26147  pntrlog2bndlem5  26149  pntrlog2bndlem6  26151  pntlemh  26167  pntlemr  26170  pntlemf  26173  pntlemk  26174  pntlemo  26175  colinearalglem4  26687  axpasch  26719  axcontlem2  26743  axcontlem4  26745  axcontlem7  26748  axcontlem8  26749  ipasslem4  28603  minvecolem2  28644  his35  28857  leopnmid  29907  ccfldsrarelvec  31044  oddpwdc  31600  prodfzo03  31862  itgexpif  31865  breprexplemc  31891  circlemeth  31899  hgt750lemg  31913  hgt750lemb  31915  hgt750leme  31917  subfacval2  32422  subfaclim  32423  circum  32905  faclimlem1  32963  faclimlem3  32965  faclim2  32968  unbdqndv2lem1  33836  knoppndvlem2  33840  knoppndvlem7  33845  knoppndvlem11  33849  knoppndvlem12  33850  knoppndvlem14  33852  knoppndvlem18  33856  itgmulc2nc  34947  areacirclem1  34969  areacirclem4  34972  bfplem1  35087  remulcan2d  39141  remul02  39220  remul01  39222  remulinvcom  39233  remulid2  39234  remulcand  39235  fltnlta  39260  cu3addd  39262  3cubeslem2  39267  3cubeslem3l  39268  3cubeslem3r  39269  pellexlem6  39416  rmxluc  39518  rmyluc2  39520  rmydbl  39522  jm2.18  39570  jm2.23  39578  jm2.27c  39589  jm3.1lem2  39600  proot1ex  39786  int-mulassocd  40515  binomcxplemnotnn0  40673  mul13d  41529  fmul01lt1lem1  41849  fmul01lt1lem2  41850  coskpi2  42131  cosknegpi  42134  dvnxpaek  42211  dvmptfprodlem  42213  dvnprodlem2  42216  itgsinexplem1  42223  stoweidlem26  42296  wallispilem5  42339  wallispi  42340  wallispi2lem1  42341  wallispi2lem2  42342  stirlinglem3  42346  stirlinglem10  42353  stirlinglem15  42358  dirkertrigeqlem1  42368  dirkertrigeqlem2  42369  dirkertrigeqlem3  42370  dirkertrigeq  42371  dirkercncflem2  42374  fourierdlem66  42442  fourierswlem  42500  fouriersw  42501  etransclem23  42527  etransclem25  42529  etransclem46  42550  hoidmvlelem2  42863  sigarls  43099  sharhght  43107  fmtnorec4  43696  fmtnoprmfac2lem1  43713  fmtnoprmfac2  43714  fmtnofac2lem  43715  fmtnofac1  43717  lighneallem4a  43758  perfectALTVlem1  43871  perfectALTVlem2  43872  perfectALTV  43873  2zrngmmgm  44202  altgsumbcALT  44386  nn0sumshdiglemB  44665  affinecomb2  44675  itscnhlc0yqe  44731  itschlc0yqe  44732  itsclc0yqsollem1  44734  itsclc0yqsol  44736  itscnhlc0xyqsol  44737  itsclc0xyqsolr  44741  itsclquadb  44748  aacllem  44887
  Copyright terms: Public domain W3C validator