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

Theorem mulcomd 9653
Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
mulcomd  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )

Proof of Theorem mulcomd
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 mulcom 9614 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1867  (class class class)co 6296   CCcc 9526    x. cmul 9533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9592
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  mul31  9790  mulcand  10234  mulcan2d  10235  divcan1  10268  divrec2  10276  div23  10278  divdivdiv  10297  divmuleq  10301  divadddiv  10311  divcan5rd  10399  dmdcan2d  10402  mvllmuld  10428  mul2lt0llt0  11389  mul2lt0lgt0  11390  xmulcom  11541  modvalr  12085  modmul12d  12130  modnegd  12131  expaddz  12302  binom3  12379  expmulnbnd  12390  digit1  12392  bccmpl  12480  bcm1k  12486  bcn2  12490  bcpasc  12492  recval  13353  abs1m  13366  reccn2  13627  lo1mul2  13659  isummulc1  13791  fsummulc1  13813  incexclem  13861  incexc  13862  trireciplem  13887  geolim  13893  cvgrat  13906  mertens  13909  ntrivcvgmul  13925  fallfacfwd  14056  bpoly4  14079  fsumcube  14080  eftlub  14130  sinadd  14185  cosadd  14186  sin2t  14198  dvds2ln  14300  oddm1even  14333  divalgmod  14351  bitsp1  14368  bitsinv1lem  14378  sadadd2lem  14396  smumullem  14429  mulgcdr  14476  rplpwr  14484  lcmgcdlem  14531  eulerthlem2  14688  prmdiv  14691  prmdivdiv  14693  vfermltlALT  14705  modprmn0modprm0  14710  coprimeprodsq  14711  pythagtriplem6  14723  pythagtriplem7  14724  pceulem  14747  pcadd  14786  prmpwdvds  14800  mul4sqlem  14849  4sqlem17OLD  14857  4sqlem17  14863  odmodnn0  17124  odmulg  17138  odmulgeq  17139  odbezout  17140  odadd1  17414  ablfacrp2  17628  pgpfac1lem3  17638  zringlpirlem3  18982  znunit  19058  icopnfhmeo  21860  cphassr  22075  pjthlem1  22265  itgabs  22666  dvmulbr  22767  dvcmul  22772  dvcmulf  22773  dvmptcmul  22792  cmvth  22817  dvlipcn  22820  c1liplem1  22822  lhop1lem  22839  lhop2  22841  dvcvx  22846  dvfsumlem2  22853  ftc1lem4  22865  itgparts  22873  dvply1  23102  elqaalem3  23139  aalioulem4  23153  taylthlem2  23191  abelthlem6  23253  abelthlem7  23255  tangtx  23322  tanarg  23430  advlogexp  23462  mulcxp  23492  cxpmul  23495  abscxp  23499  dvcxp2  23543  cxpeq  23559  ang180lem1  23600  lawcoslem1  23606  lawcos  23607  heron  23626  dcubic1  23633  mcubic  23635  cubic2  23636  binom4  23638  dquart  23641  quart1lem  23643  quart1  23644  quartlem1  23645  dvatan  23723  leibpi  23730  log2cnv  23732  efrlim  23757  cxp2lim  23764  cxploglim  23765  zetacvg  23802  lgamgulmlem2  23817  lgamgulmlem3  23818  wilthlem1  23855  ftalem1  23859  ftalem5  23863  basellem3  23869  basellem5  23871  dvdsmulf1o  23983  sgmppw  23985  logfac2  24005  chpval2  24006  chpchtsum  24007  perfect1  24016  lgsdirprm  24117  lgsdi  24120  lgsdirnn0  24127  lgsdinn0  24128  lgsquadlem1  24142  lgsquadlem2  24143  lgsquadlem3  24144  lgsquad2  24148  2sqlem3  24154  2sqlem4  24155  chebbnd1lem2  24168  chebbnd1lem3  24169  chtppilimlem2  24172  chto1lb  24176  rplogsumlem1  24182  dchrisumlem2  24188  dchrvmasum2lem  24194  dchrisum0flblem2  24207  dchrisum0lem2a  24215  mulogsumlem  24229  mulog2sumlem2  24233  selberglem1  24243  selberg2lem  24248  selberg3lem1  24255  selberg4  24259  pntrsumo1  24263  selberg34r  24269  pntrlog2bndlem3  24277  pntrlog2bndlem4  24278  pntlemb  24295  pntlemq  24299  pntlemr  24300  pntlemj  24301  pntlemo  24305  pnt2  24311  pnt  24312  padicabvcxp  24330  ostth2lem2  24332  ostth2lem3  24333  ostth2lem4  24334  ttgcontlem1  24758  brbtwn2  24778  colinearalglem1  24779  colinearalg  24783  axpaschlem  24813  axcontlem8  24844  numclwwlk1  25668  numclwwlk7  25684  smcnlem  26175  pjhthlem1  26876  kbmul  27440  kbass2  27602  2sqmod  28244  psgnfzto1st  28454  qqhval2lem  28621  qqhghm  28628  qqhrhm  28629  oddpwdc  29010  sgnmul  29198  plymulx0  29221  signsvtp  29257  signsvtn  29258  signsvfpn  29259  signsvfnn  29260  subfacval2  29695  subfaclim  29696  fwddifnp1  30714  bj-subcom  31451  bj-rdiv  31453  bj-bary1lem1  31458  itg2addnclem  31697  itg2addnclem2  31698  itgabsnc  31715  ftc1cnnclem  31719  areacirclem1  31736  areacirc  31741  geomcau  31792  bfplem1  31858  rrndstprj2  31867  rrnequiv  31871  irrapxlem5  35380  pellexlem2  35384  pellexlem6  35388  qirropth  35466  rmxyadd  35479  rmxm1  35492  rmxluc  35494  rmyluc2  35496  rmydbl  35498  jm2.24nn  35519  jm2.17a  35520  jm2.17b  35521  jm2.17c  35522  jm2.18  35553  jm2.19lem2  35555  jm2.22  35560  jm2.23  35561  areaquad  35804  imo72b2  36260  int-mulcomd  36264  int-rightdistd  36268  cvgdvgrat  36303  radcnvrat  36304  bccm1k  36332  binomcxplemwb  36338  binomcxplemnotnn0  36346  sineq0ALT  36978  mul13d  37102  subdir2d  37142  mccllem  37253  coskpi2  37317  cosknegpi  37320  dvsinax  37359  dvasinbx  37368  dvcosax  37374  dvnxpaek  37390  dvnmul  37391  dvnprodlem2  37395  itgsinexplem1  37403  stoweidlem1  37434  stoweidlem11  37444  stoweidlem26  37459  stoweidlem32  37466  wallispilem4  37503  wallispi2lem1  37506  wallispi2lem2  37507  stirlinglem3  37511  stirlinglem4  37512  stirlinglem5  37513  stirlinglem7  37515  stirlinglem10  37518  stirlinglem15  37523  dirkertrigeqlem1  37533  dirkertrigeqlem2  37534  dirkertrigeqlem3  37535  dirkertrigeq  37536  dirkercncflem1  37538  fourierdlem16  37558  fourierdlem21  37563  fourierdlem22  37564  fourierdlem56  37598  fourierdlem66  37608  fourierdlem83  37625  fourierswlem  37666  fouriersw  37667  etransclem23  37693  etransclem24  37694  etransclem38  37708  etransclem46  37716  sigarac  37865  sigarls  37870  sigarid  37871  sigardiv  37874  sigarcol  37877  sigaradd  37879  cevathlem1  37880  mod2eq1n2dvds  38128  dfeven2  38182  proththd  38317  altgsumbc  38906  altgsumbcALT  38907  blennnt2  39174  dignn0flhalflem2  39201  dignn0ehalf  39202
  Copyright terms: Public domain W3C validator