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

Theorem mulcomd 9428
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 9389 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756  (class class class)co 6112   CCcc 9301    x. cmul 9308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9367
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul31  9558  mulcand  9990  mulcan2d  9991  divcan1  10024  divrec2  10032  div23  10034  divdivdiv  10053  divmuleq  10057  divadddiv  10067  divcan5rd  10155  dmdcan2d  10158  mvllmuld  10184  xmulcom  11250  modvalr  11732  modmul12d  11774  modnegd  11775  expaddz  11929  binom3  12006  expmulnbnd  12017  digit1  12019  bccmpl  12106  bcm1k  12112  bcn2  12116  bcpasc  12118  recval  12831  abs1m  12844  reccn2  13095  lo1mul2  13127  isummulc1  13251  fsummulc1  13273  incexclem  13320  incexc  13321  trireciplem  13345  geolim  13351  cvgrat  13364  mertens  13367  eftlub  13414  sinadd  13469  cosadd  13470  sin2t  13482  dvds2ln  13584  oddm1even  13614  divalgmod  13631  bitsp1  13648  bitsinv1lem  13658  sadadd2lem  13676  smumullem  13709  mulgcdr  13753  rplpwr  13761  eulerthlem2  13878  prmdiv  13881  prmdivdiv  13883  modprmn0modprm0  13896  coprimeprodsq  13897  pythagtriplem6  13909  pythagtriplem7  13910  pceulem  13933  pcadd  13972  prmpwdvds  13986  mul4sqlem  14035  4sqlem17  14043  odmodnn0  16064  odmulg  16078  odmulgeq  16079  odbezout  16080  odadd1  16351  ablfacrp2  16590  pgpfac1lem3  16600  zringlpirlem3  17927  zlpirlem3  17932  znunit  18018  icopnfhmeo  20537  cphassr  20752  pjthlem1  20946  itgabs  21334  dvmulbr  21435  dvcmul  21440  dvcmulf  21441  dvmptcmul  21460  cmvth  21485  dvlipcn  21488  c1liplem1  21490  lhop1lem  21507  lhop2  21509  dvcvx  21514  dvfsumlem2  21521  ftc1lem4  21533  itgparts  21541  dvply1  21772  elqaalem3  21809  aalioulem4  21823  taylthlem2  21861  abelthlem6  21923  abelthlem7  21925  tangtx  21989  tanarg  22090  advlogexp  22122  mulcxp  22152  cxpmul  22155  abscxp  22159  dvcxp2  22203  cxpeq  22217  ang180lem1  22227  lawcoslem1  22233  lawcos  22234  heron  22255  dcubic1  22262  mcubic  22264  cubic2  22265  binom4  22267  dquart  22270  quart1lem  22272  quart1  22273  quartlem1  22274  dvatan  22352  leibpi  22359  log2cnv  22361  efrlim  22385  cxp2lim  22392  cxploglim  22393  wilthlem1  22428  ftalem1  22432  ftalem5  22436  basellem3  22442  basellem5  22444  dvdsmulf1o  22556  sgmppw  22558  logfac2  22578  chpval2  22579  chpchtsum  22580  perfect1  22589  lgsdirprm  22690  lgsdi  22693  lgsdirnn0  22700  lgsdinn0  22701  lgsquadlem1  22715  lgsquadlem2  22716  lgsquadlem3  22717  lgsquad2  22721  2sqlem3  22727  2sqlem4  22728  chebbnd1lem2  22741  chebbnd1lem3  22742  chtppilimlem2  22745  chto1lb  22749  rplogsumlem1  22755  dchrisumlem2  22761  dchrvmasum2lem  22767  dchrisum0flblem2  22780  dchrisum0lem2a  22788  mulogsumlem  22802  mulog2sumlem2  22806  selberglem1  22816  selberg2lem  22821  selberg3lem1  22828  selberg4  22832  pntrsumo1  22836  selberg34r  22842  pntrlog2bndlem3  22850  pntrlog2bndlem4  22851  pntlemb  22868  pntlemq  22872  pntlemr  22873  pntlemj  22874  pntlemo  22878  pnt2  22884  pnt  22885  padicabvcxp  22903  ostth2lem2  22905  ostth2lem3  22906  ostth2lem4  22907  ttgcontlem1  23153  brbtwn2  23173  colinearalglem1  23174  colinearalg  23178  axpaschlem  23208  axcontlem8  23239  smcnlem  24114  pjhthlem1  24816  kbmul  25381  kbass2  25543  mul2lt0llt0  26062  mul2lt0lgt0  26063  qqhval2lem  26432  qqhghm  26439  qqhrhm  26440  oddpwdc  26759  sgnmul  26947  plymulx0  26970  signsvtp  27006  signsvtn  27007  signsvfpn  27008  signsvfnn  27009  zetacvg  27023  lgamgulmlem2  27038  lgamgulmlem3  27039  subfacval2  27097  subfaclim  27098  ntrivcvgmul  27439  fallfacfwd  27561  bpoly4  28224  fsumcube  28225  itg2addnclem  28469  itg2addnclem2  28470  itgabsnc  28487  ftc1cnnclem  28491  areacirclem1  28510  areacirc  28515  geomcau  28681  bfplem1  28747  rrndstprj2  28756  rrnequiv  28760  irrapxlem5  29193  pellexlem2  29197  pellexlem6  29201  qirropth  29275  rmxyadd  29288  rmxm1  29301  rmxluc  29303  rmyluc2  29305  rmydbl  29307  jm2.24nn  29328  jm2.17a  29329  jm2.17b  29330  jm2.17c  29331  jm2.18  29363  jm2.19lem2  29365  jm2.22  29370  jm2.23  29371  areaquad  29618  itgsinexplem1  29820  stoweidlem1  29822  stoweidlem11  29832  stoweidlem26  29847  stoweidlem32  29853  wallispilem4  29889  wallispi2lem1  29892  wallispi2lem2  29893  stirlinglem3  29897  stirlinglem4  29898  stirlinglem5  29899  stirlinglem7  29901  stirlinglem10  29904  stirlinglem15  29909  sigarac  29914  sigarls  29919  sigarid  29920  sigardiv  29923  sigarcol  29926  sigaradd  29928  cevathlem1  29929  numclwwlk1  30717  numclwwlk7  30733  altgsumbc  30778  altgsumbcALT  30779  sineq0ALT  31769  bj-subcom  32686  bj-rdiv  32691  bj-bary1lem  32695  bj-bary1lem1  32696
  Copyright terms: Public domain W3C validator