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

Theorem mulcomd 10319
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 10279 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 579 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155  (class class class)co 6846  cc 10191   · cmul 10198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10257
This theorem depends on definitions:  df-bi 198  df-an 385
This theorem is referenced by:  mul31  10463  subdir2d  10747  mulcand  10919  mulcan2d  10920  divcan1  10953  divrec2  10961  div23  10963  divdivdiv  10985  divmuleq  10989  divadddiv  10999  divcan5rd  11087  dmdcan2d  11090  mvllmuld  11116  subhalfhalf  11517  mul2lt0llt0  12139  mul2lt0lgt0  12140  prodge0ld  12143  xmulcom  12305  modvalr  12886  mulp1mod1  12926  modmul12d  12939  modnegd  12940  modmulmodr  12951  expaddz  13118  binom3  13199  expmulnbnd  13210  digit1  13212  bccmpl  13307  bcm1k  13313  bcn2  13317  bcpasc  13319  recval  14363  abs1m  14376  reccn2  14628  lo1mul2  14660  isummulc1  14795  fsummulc1  14817  incexclem  14868  incexc  14869  trireciplem  14894  geolim  14901  cvgrat  14914  mertens  14917  ntrivcvgmul  14933  fallfacfwd  15065  bpoly4  15088  fsumcube  15089  eftlub  15137  sinadd  15192  cosadd  15193  sin2t  15205  nndivides  15291  dvds2ln  15315  even2n  15364  oddm1even  15365  mod2eq1n2dvds  15369  m1exp1  15391  pwp1fsum  15412  divalgmod  15427  bitsp1  15450  bitsinv1lem  15460  sadadd2lem  15478  smumullem  15511  mulgcdr  15564  rplpwr  15573  lcmgcdlem  15616  divgcdcoprmex  15676  cncongr1  15677  eulerthlem2  15782  prmdiv  15785  prmdivdiv  15787  vfermltlALT  15802  modprmn0modprm0  15807  coprimeprodsq  15808  pythagtriplem6  15821  pythagtriplem7  15822  pceulem  15845  pcadd  15888  prmpwdvds  15903  mul4sqlem  15952  4sqlem17  15960  mulgassr  17860  odmodnn0  18239  odmulg  18253  odmulgeq  18254  odbezout  18255  odadd1  18533  ablfacrp2  18749  pgpfac1lem3  18759  zringlpirlem3  20123  znunit  20200  icopnfhmeo  23037  cphassr  23306  pjthlem1  23513  itgabs  23908  dvmulbr  24009  dvcmul  24014  dvcmulf  24015  dvmptcmul  24034  cmvth  24061  dvlipcn  24064  c1liplem1  24066  lhop1lem  24083  lhop2  24085  dvcvx  24090  dvfsumlem2  24097  ftc1lem4  24109  itgparts  24117  dvply1  24346  elqaalem3  24383  aalioulem4  24397  taylthlem2  24435  abelthlem6  24497  abelthlem7  24499  tangtx  24565  tanarg  24672  advlogexp  24708  mulcxp  24738  cxpmul  24741  abscxp  24745  dvcxp2  24789  cxpeq  24805  ang180lem1  24846  lawcoslem1  24852  lawcos  24853  heron  24872  dcubic1  24879  mcubic  24881  cubic2  24882  binom4  24884  dquart  24887  quart1lem  24889  quart1  24890  quartlem1  24891  dvatan  24969  leibpi  24976  log2cnv  24978  efrlim  25003  cxp2lim  25010  cxploglim  25011  zetacvg  25048  lgamgulmlem2  25063  lgamgulmlem3  25064  wilthlem1  25101  ftalem1  25106  ftalem5  25110  basellem3  25116  basellem5  25118  dvdsmulf1o  25227  sgmppw  25229  logfac2  25249  chpval2  25250  chpchtsum  25251  perfect1  25260  lgsdirprm  25363  lgsdi  25366  lgsdirnn0  25376  lgsdinn0  25377  gausslemma2dlem1a  25397  gausslemma2dlem6  25404  lgsquadlem1  25412  lgsquadlem2  25413  lgsquadlem3  25414  lgsquad2  25418  2lgslem3a1  25432  2lgslem3b1  25433  2lgslem3c1  25434  2lgslem3d1  25435  2lgsoddprmlem2  25441  2sqlem3  25452  2sqlem4  25453  chebbnd1lem2  25466  chebbnd1lem3  25467  chtppilimlem2  25470  chto1lb  25474  rplogsumlem1  25480  dchrisumlem2  25486  dchrvmasum2lem  25492  dchrisum0flblem2  25505  dchrisum0lem2a  25513  mulogsumlem  25527  mulog2sumlem2  25531  selberglem1  25541  selberg2lem  25546  selberg3lem1  25553  selberg4  25557  pntrsumo1  25561  selberg34r  25567  pntrlog2bndlem3  25575  pntrlog2bndlem4  25576  pntlemb  25593  pntlemq  25597  pntlemr  25598  pntlemj  25599  pntlemo  25603  pnt2  25609  pnt  25610  padicabvcxp  25628  ostth2lem2  25630  ostth2lem3  25631  ostth2lem4  25632  ttgcontlem1  26072  brbtwn2  26092  colinearalglem1  26093  colinearalg  26097  axpaschlem  26127  axcontlem8  26158  numclwwlk1  27683  numclwwlk7  27730  smcnlem  28031  pjhthlem1  28729  kbmul  29293  kbass2  29455  2sqmod  30118  psgnfzto1st  30325  qqhval2lem  30495  qqhghm  30502  qqhrhm  30503  oddpwdc  30886  sgnmul  31075  plymulx0  31096  signsvtp  31134  signsvtn  31135  signsvfpn  31136  signsvfnn  31137  breprexplemc  31184  circlemethhgt  31195  logdivsqrle  31202  hgt750lemf  31205  hgt750lemb  31208  hgt750leme  31210  subfacval2  31640  subfaclim  31641  fwddifnp1  32739  knoppndvlem11  32975  knoppndvlem17  32981  bj-subcom  33611  bj-rdiv  33613  bj-bary1lem1  33618  itg2addnclem  33907  itg2addnclem2  33908  itgabsnc  33925  ftc1cnnclem  33929  areacirclem1  33946  areacirc  33951  geomcau  34000  bfplem1  34066  rrndstprj2  34075  rrnequiv  34079  irrapxlem5  38094  pellexlem2  38098  pellexlem6  38102  qirropth  38176  rmxyadd  38189  rmxm1  38202  rmxluc  38204  rmyluc2  38206  rmydbl  38208  jm2.24nn  38229  jm2.17a  38230  jm2.17b  38231  jm2.17c  38232  jm2.18  38258  jm2.19lem2  38260  jm2.22  38265  jm2.23  38266  areaquad  38504  imo72b2  39175  int-mulcomd  39179  int-rightdistd  39183  cvgdvgrat  39212  radcnvrat  39213  bccm1k  39241  binomcxplemwb  39247  binomcxplemnotnn0  39255  sineq0ALT  39851  mul13d  40157  divdiv3d  40239  mccllem  40493  coskpi2  40741  cosknegpi  40744  dvsinax  40791  dvasinbx  40799  dvcosax  40805  dvnxpaek  40821  dvnmul  40822  dvnprodlem2  40826  itgsinexplem1  40833  stoweidlem1  40881  stoweidlem11  40891  stoweidlem26  40906  stoweidlem32  40912  wallispilem4  40948  wallispi2lem1  40951  wallispi2lem2  40952  stirlinglem3  40956  stirlinglem4  40957  stirlinglem5  40958  stirlinglem7  40960  stirlinglem10  40963  stirlinglem15  40968  dirkertrigeqlem1  40978  dirkertrigeqlem2  40979  dirkertrigeqlem3  40980  dirkertrigeq  40981  dirkercncflem1  40983  fourierdlem16  41003  fourierdlem21  41008  fourierdlem22  41009  fourierdlem56  41042  fourierdlem66  41052  fourierdlem83  41069  fourierswlem  41110  fouriersw  41111  etransclem23  41137  etransclem24  41138  etransclem38  41152  etransclem46  41160  hoiprodp1  41468  hoidmvlelem2  41476  smfmullem1  41664  sigarac  41707  sigarls  41712  sigarid  41713  sigardiv  41716  sigarcol  41719  sigaradd  41721  cevathlem1  41722  fmtnoodd  42147  sqrtpwpw2p  42152  fmtnorec3  42162  fmtnoprmfac2lem1  42180  fmtnofac1  42184  pwdif  42203  lighneallem2  42225  lighneallem3  42226  proththd  42233  dfeven2  42264  altgsumbc  42825  altgsumbcALT  42826  blennnt2  43078  dignn0flhalflem2  43105  dignn0ehalf  43106  amgmwlem  43246
  Copyright terms: Public domain W3C validator