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

Theorem mulcomd 9917
Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
mulcomd (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcomd
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 mulcom 9878 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 690 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9790   · cmul 9797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9856
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  mul31  10055  mulcand  10509  mulcan2d  10510  divcan1  10543  divrec2  10551  div23  10553  divdivdiv  10575  divmuleq  10579  divadddiv  10589  divcan5rd  10677  dmdcan2d  10680  mvllmuld  10706  subhalfhalf  11113  mul2lt0llt0  11766  mul2lt0lgt0  11767  xmulcom  11925  modvalr  12488  mulp1mod1  12528  modmul12d  12541  modnegd  12542  modmulmodr  12553  expaddz  12721  binom3  12802  expmulnbnd  12813  digit1  12815  bccmpl  12913  bcm1k  12919  bcn2  12923  bcpasc  12925  recval  13856  abs1m  13869  reccn2  14121  lo1mul2  14153  isummulc1  14282  fsummulc1  14305  incexclem  14353  incexc  14354  trireciplem  14379  geolim  14386  cvgrat  14400  mertens  14403  ntrivcvgmul  14419  fallfacfwd  14552  bpoly4  14575  fsumcube  14576  eftlub  14624  sinadd  14679  cosadd  14680  sin2t  14692  nndivides  14774  dvds2ln  14798  even2n  14850  oddm1even  14851  mod2eq1n2dvds  14855  m1exp1  14877  pwp1fsum  14898  divalgmod  14913  divalgmodOLD  14914  bitsp1  14937  bitsinv1lem  14947  sadadd2lem  14965  smumullem  14998  mulgcdr  15051  rplpwr  15060  lcmgcdlem  15103  divgcdcoprmex  15164  cncongr1  15165  eulerthlem2  15271  prmdiv  15274  prmdivdiv  15276  vfermltlALT  15291  modprmn0modprm0  15296  coprimeprodsq  15297  pythagtriplem6  15310  pythagtriplem7  15311  pceulem  15334  pcadd  15377  prmpwdvds  15392  mul4sqlem  15441  4sqlem17  15449  mulgassr  17349  odmodnn0  17728  odmulg  17742  odmulgeq  17743  odbezout  17744  odadd1  18020  ablfacrp2  18235  pgpfac1lem3  18245  zringlpirlem3  19599  znunit  19676  icopnfhmeo  22481  cphassr  22743  pjthlem1  22933  itgabs  23324  dvmulbr  23425  dvcmul  23430  dvcmulf  23431  dvmptcmul  23450  cmvth  23475  dvlipcn  23478  c1liplem1  23480  lhop1lem  23497  lhop2  23499  dvcvx  23504  dvfsumlem2  23511  ftc1lem4  23523  itgparts  23531  dvply1  23760  elqaalem3  23797  aalioulem4  23811  taylthlem2  23849  abelthlem6  23911  abelthlem7  23913  tangtx  23978  tanarg  24086  advlogexp  24118  mulcxp  24148  cxpmul  24151  abscxp  24155  dvcxp2  24199  cxpeq  24215  ang180lem1  24256  lawcoslem1  24262  lawcos  24263  heron  24282  dcubic1  24289  mcubic  24291  cubic2  24292  binom4  24294  dquart  24297  quart1lem  24299  quart1  24300  quartlem1  24301  dvatan  24379  leibpi  24386  log2cnv  24388  efrlim  24413  cxp2lim  24420  cxploglim  24421  zetacvg  24458  lgamgulmlem2  24473  lgamgulmlem3  24474  wilthlem1  24511  ftalem1  24516  ftalem5  24520  basellem3  24526  basellem5  24528  dvdsmulf1o  24637  sgmppw  24639  logfac2  24659  chpval2  24660  chpchtsum  24661  perfect1  24670  lgsdirprm  24773  lgsdi  24776  lgsdirnn0  24786  lgsdinn0  24787  gausslemma2dlem1a  24807  gausslemma2dlem6  24814  lgsquadlem1  24822  lgsquadlem2  24823  lgsquadlem3  24824  lgsquad2  24828  2lgslem3a1  24842  2lgslem3b1  24843  2lgslem3c1  24844  2lgslem3d1  24845  2lgsoddprmlem2  24851  2sqlem3  24862  2sqlem4  24863  chebbnd1lem2  24876  chebbnd1lem3  24877  chtppilimlem2  24880  chto1lb  24884  rplogsumlem1  24890  dchrisumlem2  24896  dchrvmasum2lem  24902  dchrisum0flblem2  24915  dchrisum0lem2a  24923  mulogsumlem  24937  mulog2sumlem2  24941  selberglem1  24951  selberg2lem  24956  selberg3lem1  24963  selberg4  24967  pntrsumo1  24971  selberg34r  24977  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntlemb  25003  pntlemq  25007  pntlemr  25008  pntlemj  25009  pntlemo  25013  pnt2  25019  pnt  25020  padicabvcxp  25038  ostth2lem2  25040  ostth2lem3  25041  ostth2lem4  25042  ttgcontlem1  25483  brbtwn2  25503  colinearalglem1  25504  colinearalg  25508  axpaschlem  25538  axcontlem8  25569  numclwwlk1  26391  numclwwlk7  26407  smcnlem  26737  pjhthlem1  27440  kbmul  28004  kbass2  28166  2sqmod  28785  psgnfzto1st  28992  qqhval2lem  29159  qqhghm  29166  qqhrhm  29167  oddpwdc  29549  sgnmul  29737  plymulx0  29756  signsvtp  29792  signsvtn  29793  signsvfpn  29794  signsvfnn  29795  subfacval2  30229  subfaclim  30230  fwddifnp1  31248  knoppndvlem11  31489  knoppndvlem17  31495  bj-subcom  32127  bj-rdiv  32129  bj-bary1lem1  32134  itg2addnclem  32427  itg2addnclem2  32428  itgabsnc  32445  ftc1cnnclem  32449  areacirclem1  32466  areacirc  32471  geomcau  32521  bfplem1  32587  rrndstprj2  32596  rrnequiv  32600  irrapxlem5  36204  pellexlem2  36208  pellexlem6  36212  qirropth  36287  rmxyadd  36300  rmxm1  36313  rmxluc  36315  rmyluc2  36317  rmydbl  36319  jm2.24nn  36340  jm2.17a  36341  jm2.17b  36342  jm2.17c  36343  jm2.18  36369  jm2.19lem2  36371  jm2.22  36376  jm2.23  36377  areaquad  36617  imo72b2  37293  int-mulcomd  37297  int-rightdistd  37301  cvgdvgrat  37330  radcnvrat  37331  bccm1k  37359  binomcxplemwb  37365  binomcxplemnotnn0  37373  sineq0ALT  37991  mul13d  38228  subdir2d  38262  divdiv3d  38313  mccllem  38461  coskpi2  38546  cosknegpi  38549  dvsinax  38598  dvasinbx  38607  dvcosax  38613  dvnxpaek  38629  dvnmul  38630  dvnprodlem2  38634  itgsinexplem1  38642  stoweidlem1  38691  stoweidlem11  38701  stoweidlem26  38716  stoweidlem32  38722  wallispilem4  38758  wallispi2lem1  38761  wallispi2lem2  38762  stirlinglem3  38766  stirlinglem4  38767  stirlinglem5  38768  stirlinglem7  38770  stirlinglem10  38773  stirlinglem15  38778  dirkertrigeqlem1  38788  dirkertrigeqlem2  38789  dirkertrigeqlem3  38790  dirkertrigeq  38791  dirkercncflem1  38793  fourierdlem16  38813  fourierdlem21  38818  fourierdlem22  38819  fourierdlem56  38852  fourierdlem66  38862  fourierdlem83  38879  fourierswlem  38920  fouriersw  38921  etransclem23  38947  etransclem24  38948  etransclem38  38962  etransclem46  38970  hoiprodp1  39275  hoidmvlelem2  39283  smfmullem1  39473  sigarac  39487  sigarls  39492  sigarid  39493  sigardiv  39496  sigarcol  39499  sigaradd  39501  cevathlem1  39502  fmtnoodd  39781  sqrtpwpw2p  39786  fmtnorec3  39796  fmtnoprmfac2lem1  39814  fmtnofac1  39818  pwdif  39837  lighneallem2  39859  lighneallem3  39860  proththd  39867  dfeven2  39898  av-numclwwlk1  41523  av-numclwwlk7  41540  altgsumbc  41918  altgsumbcALT  41919  blennnt2  42176  dignn0flhalflem2  42203  dignn0ehalf  42204  amgmwlem  42313
  Copyright terms: Public domain W3C validator