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

Theorem mulcomd 9065
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 9032 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721  (class class class)co 6040   CCcc 8944    x. cmul 8951
This theorem is referenced by:  mul31  9190  mulcand  9611  mulcan2d  9612  divcan1  9643  divrec2  9651  div23  9653  divdivdiv  9671  divmuleq  9675  divadddiv  9685  divcan5rd  9773  dmdcan2d  9776  xmulcom  10801  modmul12d  11235  modnegd  11236  expaddz  11379  binom3  11455  expmulnbnd  11466  digit1  11468  bccmpl  11555  bcm1k  11561  bcn2  11565  bcpasc  11567  recval  12081  abs1m  12094  reccn2  12345  lo1mul2  12377  isummulc1  12502  fsummulc1  12523  incexclem  12571  incexc  12572  trireciplem  12596  geolim  12602  cvgrat  12615  mertens  12618  eftlub  12665  sinadd  12720  cosadd  12721  sin2t  12733  dvds2ln  12835  oddm1even  12864  divalgmod  12881  bitsp1  12898  bitsinv1lem  12908  sadadd2lem  12926  smumullem  12959  mulgcdr  13003  rplpwr  13011  eulerthlem2  13126  prmdiv  13129  prmdivdiv  13131  coprimeprodsq  13138  pythagtriplem6  13150  pythagtriplem7  13151  pceulem  13174  pcadd  13213  prmpwdvds  13227  mul4sqlem  13276  4sqlem17  13284  odmodnn0  15133  odmulg  15147  odmulgeq  15148  odbezout  15149  odadd1  15418  ablfacrp2  15580  pgpfac1lem3  15590  zlpirlem3  16725  znunit  16799  icopnfhmeo  18921  cphassr  19127  pjthlem1  19291  itgabs  19679  dvmulbr  19778  dvcmul  19783  dvcmulf  19784  dvmptcmul  19803  cmvth  19828  dvlipcn  19831  c1liplem1  19833  lhop1lem  19850  lhop2  19852  dvcvx  19857  dvfsumlem2  19864  ftc1lem4  19876  itgparts  19884  dvply1  20154  elqaalem3  20191  aalioulem4  20205  taylthlem2  20243  abelthlem6  20305  abelthlem7  20307  tangtx  20366  tanarg  20467  advlogexp  20499  mulcxp  20529  cxpmul  20532  abscxp  20536  dvcxp2  20580  cxpeq  20594  ang180lem1  20604  lawcoslem1  20610  lawcos  20611  dcubic1  20638  mcubic  20640  cubic2  20641  binom4  20643  dquart  20646  quart1lem  20648  quart1  20649  quartlem1  20650  dvatan  20728  leibpi  20735  log2cnv  20737  efrlim  20761  cxp2lim  20768  cxploglim  20769  wilthlem1  20804  ftalem1  20808  ftalem5  20812  basellem3  20818  basellem5  20820  dvdsmulf1o  20932  sgmppw  20934  logfac2  20954  chpval2  20955  chpchtsum  20956  perfect1  20965  lgsdirprm  21066  lgsdi  21069  lgsdirnn0  21076  lgsdinn0  21077  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad2  21097  2sqlem3  21103  2sqlem4  21104  chebbnd1lem2  21117  chebbnd1lem3  21118  chtppilimlem2  21121  chto1lb  21125  rplogsumlem1  21131  dchrisumlem2  21137  dchrvmasum2lem  21143  dchrisum0flblem2  21156  dchrisum0lem2a  21164  mulogsumlem  21178  mulog2sumlem2  21182  selberglem1  21192  selberg2lem  21197  selberg3lem1  21204  selberg4  21208  pntrsumo1  21212  selberg34r  21218  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntlemb  21244  pntlemq  21248  pntlemr  21249  pntlemj  21250  pntlemo  21254  pnt2  21260  pnt  21261  padicabvcxp  21279  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  smcnlem  22146  pjhthlem1  22846  kbmul  23411  kbass2  23573  qqhval2lem  24318  qqhghm  24325  qqhrhm  24326  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem3  24768  subfacval2  24826  subfaclim  24827  ntrivcvgmul  25183  fallfacfwd  25303  brbtwn2  25748  colinearalglem1  25749  colinearalg  25753  axpaschlem  25783  axcontlem8  25814  bpoly4  26009  fsumcube  26010  itg2addnclem  26155  itg2addnclem2  26156  itgabsnc  26173  ftc1cnnclem  26177  areacirclem2  26181  areacirc  26187  geomcau  26355  bfplem1  26421  rrndstprj2  26430  rrnequiv  26434  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  qirropth  26861  rmxyadd  26874  rmxm1  26887  rmxluc  26889  rmyluc2  26891  rmydbl  26893  jm2.24nn  26914  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  jm2.18  26949  jm2.19lem2  26951  jm2.22  26956  jm2.23  26957  itgsinexplem1  27615  stoweidlem1  27617  stoweidlem11  27627  stoweidlem26  27642  stoweidlem32  27648  wallispilem4  27684  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem7  27696  stirlinglem10  27699  stirlinglem15  27704  sigarac  27709  sigarls  27714  sigarid  27715  sigardiv  27718  sigarcol  27721  sigaradd  27723  cevathlem1  27724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcom 9010
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator