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

Theorem mulassd 9920
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 9881 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1317 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9791   · cmul 9798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9859
This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032
This theorem is referenced by:  recex  10511  mulcand  10512  receu  10524  divmulasscom  10561  divdivdiv  10578  divmuleq  10582  conjmul  10594  modmul1  12543  moddi  12558  expadd  12722  mulbinom2  12804  binom3  12805  digit1  12818  discr1  12820  discr  12821  faclbnd  12897  faclbnd6  12906  bcm1k  12922  bcp1nk  12924  crre  13651  remullem  13665  amgm2  13906  iseraltlem2  14210  iseraltlem3  14211  binomlem  14349  climcndslem2  14370  geo2sum  14392  mertenslem1  14404  clim2prod  14408  fallrisefac  14544  binomfallfaclem2  14559  bpolydiflem  14573  bpoly4  14578  sinadd  14682  tanadd  14685  pwp1fsum  14901  bezoutlem3  15045  dvdsmulgcd  15061  qredeq  15158  pcaddlem  15379  prmpwdvds  15395  ablfacrp  18237  nmoco  22299  cph2ass  22766  cphipval2  22793  csbren  22935  minveclem2  22950  uniioombllem5  23106  itg1mulc  23222  mbfi1fseqlem5  23237  itgconst  23336  itgmulc2  23351  dvexp  23467  dvply1  23788  elqaalem3  23825  aalioulem1  23836  aaliou3lem2  23847  dvtaylp  23873  dvradcnv  23924  pserdvlem2  23931  tangtx  24006  tanregt0  24034  tanarg  24114  logcnlem4  24136  cxpmul  24179  dvcxp1  24226  dvcncxp1  24229  root1eq1  24241  heron  24310  quad2  24311  dcubic1lem  24315  dcubic1  24317  cubic2  24320  binom4  24322  dquartlem1  24323  dquartlem2  24324  dquart  24325  quart1lem  24327  quart1  24328  quartlem1  24329  efiasin  24360  asinsinlem  24363  asinsin  24364  efiatan  24384  efiatan2  24389  2efiatan  24390  atantan  24395  atanbndlem  24397  atans2  24403  atantayl  24409  log2cnv  24416  log2tlbnd  24417  ftalem1  24544  ftalem5  24548  basellem3  24554  basellem5  24556  basellem8  24559  chtub  24682  perfectlem1  24699  perfectlem2  24700  perfect  24701  bcmono  24747  bclbnd  24750  bposlem9  24762  lgsneg  24791  gausslemma2dlem6  24842  lgseisenlem1  24845  lgseisenlem2  24846  lgseisenlem3  24847  lgseisenlem4  24848  lgsquad2lem1  24854  lgsquad3  24857  2lgslem3a  24866  2lgslem3b  24867  2lgslem3c  24868  2lgslem3d  24869  2lgsoddprmlem2  24879  2sqlem3  24890  chto1ub  24910  rplogsumlem1  24918  dchrmusum2  24928  dchrvmasum2lem  24930  dchrvmasumlem2  24932  dchrvmasumiflem2  24936  dchrisum0lem1  24950  dchrisum0lem2  24952  mulog2sumlem2  24969  chpdifbndlem1  24987  selberg3lem1  24991  selberg4lem1  24994  selberg34r  25005  pntrlog2bndlem3  25013  pntrlog2bndlem5  25015  pntrlog2bndlem6  25017  pntlemh  25033  pntlemr  25036  pntlemf  25039  pntlemk  25040  pntlemo  25041  colinearalglem4  25535  axpasch  25567  axcontlem2  25591  axcontlem4  25593  axcontlem7  25596  axcontlem8  25597  ipasslem4  26907  minvecolem2  26949  his35  27163  leopnmid  28215  oddpwdc  29577  subfacval2  30257  subfaclim  30258  circum  30656  faclimlem1  30716  faclimlem3  30718  faclim2  30721  unbdqndv2lem1  31504  knoppndvlem2  31508  knoppndvlem7  31513  knoppndvlem11  31517  knoppndvlem12  31518  knoppndvlem14  31520  knoppndvlem18  31524  itgmulc2nc  32472  areacirclem1  32494  areacirclem4  32497  bfplem1  32615  pellexlem6  36240  rmxluc  36343  rmyluc2  36345  rmydbl  36347  jm2.18  36397  jm2.23  36405  jm2.27c  36416  jm3.1lem2  36427  proot1ex  36622  int-mulassocd  37326  binomcxplemnotnn0  37401  mul13d  38256  fmul01lt1lem1  38475  fmul01lt1lem2  38476  coskpi2  38573  cosknegpi  38576  dvnxpaek  38656  dvmptfprodlem  38658  dvnprodlem2  38661  itgsinexplem1  38669  stoweidlem26  38743  wallispilem5  38786  wallispi  38787  wallispi2lem1  38788  wallispi2lem2  38789  stirlinglem3  38793  stirlinglem10  38800  stirlinglem15  38805  dirkertrigeqlem1  38815  dirkertrigeqlem2  38816  dirkertrigeqlem3  38817  dirkertrigeq  38818  dirkercncflem2  38821  fourierdlem66  38889  fourierswlem  38947  fouriersw  38948  etransclem23  38974  etransclem25  38976  etransclem46  38997  hoidmvlelem2  39310  sigarls  39519  sharhght  39527  fmtnorec4  39824  fmtnoprmfac2lem1  39841  fmtnoprmfac2  39842  fmtnofac2lem  39843  fmtnofac1  39845  pwdif  39864  lighneallem4a  39888  perfectALTVlem1  39989  perfectALTVlem2  39990  perfectALTV  39991  2zrngmmgm  41758  altgsumbcALT  41946  nn0sumshdiglemB  42234  aacllem  42339
  Copyright terms: Public domain W3C validator