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

Theorem mulassd 10317
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 10277 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1490 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155  (class class class)co 6842  cc 10187   · cmul 10194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10255
This theorem depends on definitions:  df-bi 198  df-an 385  df-3an 1109
This theorem is referenced by:  recex  10913  mulcand  10914  receu  10926  divmulasscom  10963  divdivdiv  10980  divmuleq  10984  conjmul  10996  modmul1  12931  moddi  12946  expadd  13109  mulbinom2  13191  binom3  13192  digit1  13205  discr1  13207  discr  13208  faclbnd  13281  faclbnd6  13290  bcm1k  13306  bcp1nk  13308  crre  14139  remullem  14153  amgm2  14394  iseraltlem2  14698  iseraltlem3  14699  binomlem  14845  climcndslem2  14866  geo2sum  14888  mertenslem1  14899  clim2prod  14903  fallrisefac  15038  binomfallfaclem2  15053  bpolydiflem  15067  bpoly4  15072  sinadd  15176  tanadd  15179  pwp1fsum  15396  bezoutlem3  15539  dvdsmulgcd  15555  qredeq  15651  pcaddlem  15871  prmpwdvds  15887  ablfacrp  18732  nmoco  22820  cph2ass  23291  cphipval2  23318  csbren  23471  minveclem2  23486  uniioombllem5  23645  itg1mulc  23762  mbfi1fseqlem5  23777  itgconst  23876  itgmulc2  23891  dvexp  24007  dvply1  24330  elqaalem3  24367  aalioulem1  24378  aaliou3lem2  24389  dvtaylp  24415  dvradcnv  24466  pserdvlem2  24473  tangtx  24549  tanregt0  24577  tanarg  24656  logcnlem4  24682  cxpmul  24725  dvcxp1  24772  dvcncxp1  24775  root1eq1  24787  heron  24856  quad2  24857  dcubic1lem  24861  dcubic1  24863  cubic2  24866  binom4  24868  dquartlem1  24869  dquartlem2  24870  dquart  24871  quart1lem  24873  quart1  24874  quartlem1  24875  efiasin  24906  asinsinlem  24909  asinsin  24910  efiatan  24930  efiatan2  24935  2efiatan  24936  atantan  24941  atanbndlem  24943  atans2  24949  atantayl  24955  log2cnv  24962  log2tlbnd  24963  ftalem1  25090  ftalem5  25094  basellem3  25100  basellem5  25102  basellem8  25105  chtub  25228  perfectlem1  25245  perfectlem2  25246  perfect  25247  bcmono  25293  bclbnd  25296  bposlem9  25308  lgsneg  25337  gausslemma2dlem6  25388  lgseisenlem1  25391  lgseisenlem2  25392  lgseisenlem3  25393  lgseisenlem4  25394  lgsquad2lem1  25400  lgsquad3  25403  2lgslem3a  25412  2lgslem3b  25413  2lgslem3c  25414  2lgslem3d  25415  2lgsoddprmlem2  25425  2sqlem3  25436  chto1ub  25456  rplogsumlem1  25464  dchrmusum2  25474  dchrvmasum2lem  25476  dchrvmasumlem2  25478  dchrvmasumiflem2  25482  dchrisum0lem1  25496  dchrisum0lem2  25498  mulog2sumlem2  25515  chpdifbndlem1  25533  selberg3lem1  25537  selberg4lem1  25540  selberg34r  25551  pntrlog2bndlem3  25559  pntrlog2bndlem5  25561  pntrlog2bndlem6  25563  pntlemh  25579  pntlemr  25582  pntlemf  25585  pntlemk  25586  pntlemo  25587  colinearalglem4  26080  axpasch  26112  axcontlem2  26136  axcontlem4  26138  axcontlem7  26141  axcontlem8  26142  ipasslem4  28145  minvecolem2  28187  his35  28401  leopnmid  29453  oddpwdc  30863  prodfzo03  31132  itgexpif  31135  breprexplemc  31161  circlemeth  31169  hgt750lemg  31183  hgt750lemb  31185  hgt750leme  31187  subfacval2  31617  subfaclim  31618  circum  32014  faclimlem1  32074  faclimlem3  32076  faclim2  32079  unbdqndv2lem1  32939  knoppndvlem2  32943  knoppndvlem7  32948  knoppndvlem11  32952  knoppndvlem12  32953  knoppndvlem14  32955  knoppndvlem18  32959  itgmulc2nc  33901  areacirclem1  33923  areacirclem4  33926  bfplem1  34043  pellexlem6  38076  rmxluc  38178  rmyluc2  38180  rmydbl  38182  jm2.18  38232  jm2.23  38240  jm2.27c  38251  jm3.1lem2  38262  proot1ex  38456  int-mulassocd  39154  binomcxplemnotnn0  39229  mul13d  40131  fmul01lt1lem1  40454  fmul01lt1lem2  40455  coskpi2  40715  cosknegpi  40718  dvnxpaek  40795  dvmptfprodlem  40797  dvnprodlem2  40800  itgsinexplem1  40807  stoweidlem26  40880  wallispilem5  40923  wallispi  40924  wallispi2lem1  40925  wallispi2lem2  40926  stirlinglem3  40930  stirlinglem10  40937  stirlinglem15  40942  dirkertrigeqlem1  40952  dirkertrigeqlem2  40953  dirkertrigeqlem3  40954  dirkertrigeq  40955  dirkercncflem2  40958  fourierdlem66  41026  fourierswlem  41084  fouriersw  41085  etransclem23  41111  etransclem25  41113  etransclem46  41134  hoidmvlelem2  41450  sigarls  41686  sharhght  41694  fmtnorec4  42137  fmtnoprmfac2lem1  42154  fmtnoprmfac2  42155  fmtnofac2lem  42156  fmtnofac1  42158  pwdif  42177  lighneallem4a  42201  perfectALTVlem1  42306  perfectALTVlem2  42307  perfectALTV  42308  2zrngmmgm  42615  altgsumbcALT  42800  nn0sumshdiglemB  43083  aacllem  43219
  Copyright terms: Public domain W3C validator