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

Theorem mulcomd 9664
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 9625 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 667 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    e. wcel 1887  (class class class)co 6290   CCcc 9537    x. cmul 9544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9603
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  mul31  9801  mulcand  10245  mulcan2d  10246  divcan1  10279  divrec2  10287  div23  10289  divdivdiv  10308  divmuleq  10312  divadddiv  10322  divcan5rd  10410  dmdcan2d  10413  mvllmuld  10439  mul2lt0llt0  11400  mul2lt0lgt0  11401  xmulcom  11552  modvalr  12099  modmul12d  12144  modnegd  12145  expaddz  12316  binom3  12393  expmulnbnd  12404  digit1  12406  bccmpl  12494  bcm1k  12500  bcn2  12504  bcpasc  12506  recval  13385  abs1m  13398  reccn2  13660  lo1mul2  13692  isummulc1  13824  fsummulc1  13846  incexclem  13894  incexc  13895  trireciplem  13920  geolim  13926  cvgrat  13939  mertens  13942  ntrivcvgmul  13958  fallfacfwd  14089  bpoly4  14112  fsumcube  14113  eftlub  14163  sinadd  14218  cosadd  14219  sin2t  14231  dvds2ln  14333  oddm1even  14366  divalgmod  14387  bitsp1  14404  bitsinv1lem  14415  sadadd2lem  14433  smumullem  14466  mulgcdr  14516  rplpwr  14524  lcmgcdlem  14571  eulerthlem2  14730  prmdiv  14733  prmdivdiv  14735  vfermltlALT  14753  modprmn0modprm0  14758  coprimeprodsq  14759  pythagtriplem6  14771  pythagtriplem7  14772  pceulem  14795  pcadd  14834  prmpwdvds  14848  mul4sqlem  14897  4sqlem17OLD  14905  4sqlem17  14911  odmodnn0  17189  odmulg  17207  odmulgeq  17208  odbezout  17209  odadd1  17486  ablfacrp2  17700  pgpfac1lem3  17710  zringlpirlem3OLD  19055  zringlpirlem3  19057  znunit  19134  icopnfhmeo  21971  cphassr  22189  pjthlem1  22391  itgabs  22792  dvmulbr  22893  dvcmul  22898  dvcmulf  22899  dvmptcmul  22918  cmvth  22943  dvlipcn  22946  c1liplem1  22948  lhop1lem  22965  lhop2  22967  dvcvx  22972  dvfsumlem2  22979  ftc1lem4  22991  itgparts  22999  dvply1  23237  elqaalem3  23274  elqaalem3OLD  23277  aalioulem4  23291  taylthlem2  23329  abelthlem6  23391  abelthlem7  23393  tangtx  23460  tanarg  23568  advlogexp  23600  mulcxp  23630  cxpmul  23633  abscxp  23637  dvcxp2  23681  cxpeq  23697  ang180lem1  23738  lawcoslem1  23744  lawcos  23745  heron  23764  dcubic1  23771  mcubic  23773  cubic2  23774  binom4  23776  dquart  23779  quart1lem  23781  quart1  23782  quartlem1  23783  dvatan  23861  leibpi  23868  log2cnv  23870  efrlim  23895  cxp2lim  23902  cxploglim  23903  zetacvg  23940  lgamgulmlem2  23955  lgamgulmlem3  23956  wilthlem1  23993  ftalem1  23997  ftalem5  24001  ftalem5OLD  24003  basellem3  24009  basellem5  24011  dvdsmulf1o  24123  sgmppw  24125  logfac2  24145  chpval2  24146  chpchtsum  24147  perfect1  24156  lgsdirprm  24257  lgsdi  24260  lgsdirnn0  24267  lgsdinn0  24268  lgsquadlem1  24282  lgsquadlem2  24283  lgsquadlem3  24284  lgsquad2  24288  2sqlem3  24294  2sqlem4  24295  chebbnd1lem2  24308  chebbnd1lem3  24309  chtppilimlem2  24312  chto1lb  24316  rplogsumlem1  24322  dchrisumlem2  24328  dchrvmasum2lem  24334  dchrisum0flblem2  24347  dchrisum0lem2a  24355  mulogsumlem  24369  mulog2sumlem2  24373  selberglem1  24383  selberg2lem  24388  selberg3lem1  24395  selberg4  24399  pntrsumo1  24403  selberg34r  24409  pntrlog2bndlem3  24417  pntrlog2bndlem4  24418  pntlemb  24435  pntlemq  24439  pntlemr  24440  pntlemj  24441  pntlemo  24445  pnt2  24451  pnt  24452  padicabvcxp  24470  ostth2lem2  24472  ostth2lem3  24473  ostth2lem4  24474  ttgcontlem1  24915  brbtwn2  24935  colinearalglem1  24936  colinearalg  24940  axpaschlem  24970  axcontlem8  25001  numclwwlk1  25826  numclwwlk7  25842  smcnlem  26333  pjhthlem1  27044  kbmul  27608  kbass2  27770  2sqmod  28409  psgnfzto1st  28618  qqhval2lem  28785  qqhghm  28792  qqhrhm  28793  oddpwdc  29187  sgnmul  29413  plymulx0  29436  signsvtp  29472  signsvtn  29473  signsvfpn  29474  signsvfnn  29475  subfacval2  29910  subfaclim  29911  fwddifnp1  30932  bj-subcom  31709  bj-rdiv  31711  bj-bary1lem1  31716  itg2addnclem  31993  itg2addnclem2  31994  itgabsnc  32011  ftc1cnnclem  32015  areacirclem1  32032  areacirc  32037  geomcau  32088  bfplem1  32154  rrndstprj2  32163  rrnequiv  32167  irrapxlem5  35670  pellexlem2  35674  pellexlem6  35678  qirropth  35756  rmxyadd  35769  rmxm1  35782  rmxluc  35784  rmyluc2  35786  rmydbl  35788  jm2.24nn  35809  jm2.17a  35810  jm2.17b  35811  jm2.17c  35812  jm2.18  35843  jm2.19lem2  35845  jm2.22  35850  jm2.23  35851  areaquad  36101  imo72b2  36619  int-mulcomd  36623  int-rightdistd  36627  cvgdvgrat  36662  radcnvrat  36663  bccm1k  36691  binomcxplemwb  36697  binomcxplemnotnn0  36705  sineq0ALT  37334  mul13d  37489  subdir2d  37529  divdiv3d  37582  mccllem  37677  coskpi2  37741  cosknegpi  37744  dvsinax  37783  dvasinbx  37792  dvcosax  37798  dvnxpaek  37817  dvnmul  37818  dvnprodlem2  37822  itgsinexplem1  37830  stoweidlem1  37861  stoweidlem11  37871  stoweidlem26  37886  stoweidlem32  37893  wallispilem4  37930  wallispi2lem1  37933  wallispi2lem2  37934  stirlinglem3  37938  stirlinglem4  37939  stirlinglem5  37940  stirlinglem7  37942  stirlinglem10  37945  stirlinglem15  37950  dirkertrigeqlem1  37960  dirkertrigeqlem2  37961  dirkertrigeqlem3  37962  dirkertrigeq  37963  dirkercncflem1  37965  fourierdlem16  37985  fourierdlem21  37990  fourierdlem22  37991  fourierdlem56  38026  fourierdlem66  38036  fourierdlem83  38053  fourierswlem  38094  fouriersw  38095  etransclem23  38122  etransclem24  38123  etransclem38  38137  etransclem46  38145  hoiprodp1  38410  hoidmvlelem2  38418  sigarac  38461  sigarls  38466  sigarid  38467  sigardiv  38470  sigarcol  38473  sigaradd  38475  cevathlem1  38476  mod2eq1n2dvds  38725  dfeven2  38779  proththd  38914  altgsumbc  40186  altgsumbcALT  40187  blennnt2  40453  dignn0flhalflem2  40480  dignn0ehalf  40481
  Copyright terms: Public domain W3C validator