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

Theorem mulcomd 8872
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 8839 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    x. cmul 8758
This theorem is referenced by:  mul31  8996  mulcand  9417  mulcan2d  9418  divcan1  9449  divrec2  9457  div23  9459  divdivdiv  9477  divmuleq  9481  divadddiv  9491  divcan5rd  9579  dmdcan2d  9582  xmulcom  10602  modmul12d  11019  modnegd  11020  expaddz  11162  binom3  11238  expmulnbnd  11249  digit1  11251  bccmpl  11338  bcm1k  11343  bcp1nk  11345  bcn2  11347  bcpasc  11349  recval  11822  abs1m  11835  reccn2  12086  lo1mul2  12118  isummulc1  12242  fsummulc1  12263  incexclem  12311  incexc  12312  trireciplem  12336  geolim  12342  cvgrat  12355  mertens  12358  eftlub  12405  sinadd  12460  cosadd  12461  sin2t  12473  dvds2ln  12575  oddm1even  12604  divalgmod  12621  bitsp1  12638  bitsinv1lem  12648  sadadd2lem  12666  smumullem  12699  mulgcdr  12743  rplpwr  12751  eulerthlem2  12866  prmdiv  12869  prmdivdiv  12871  coprimeprodsq  12878  pythagtriplem6  12890  pythagtriplem7  12891  pceulem  12914  pcadd  12953  prmpwdvds  12967  mul4sqlem  13016  4sqlem17  13024  odmodnn0  14871  odmulg  14885  odmulgeq  14886  odbezout  14887  odadd1  15156  ablfacrp2  15318  pgpfac1lem3  15328  zlpirlem3  16459  znunit  16533  icopnfhmeo  18457  cphassr  18663  pjthlem1  18817  itgabs  19205  dvmulbr  19304  dvcmul  19309  dvcmulf  19310  dvcobr  19311  dvmptcmul  19329  cmvth  19354  dvlipcn  19357  c1liplem1  19359  lhop1lem  19376  lhop2  19378  dvcvx  19383  dvfsumlem2  19390  ftc1lem4  19402  itgparts  19410  dvply1  19680  elqaalem3  19717  aalioulem4  19731  taylthlem2  19769  abelthlem6  19828  abelthlem7  19830  tangtx  19889  tanarg  19986  advlogexp  20018  mulcxp  20048  cxpmul  20051  abscxp  20055  dvcxp2  20099  cxpeq  20113  ang180lem1  20123  lawcoslem1  20129  lawcos  20130  dcubic1  20157  mcubic  20159  cubic2  20160  binom4  20162  dquart  20165  quart1lem  20167  quart1  20168  quartlem1  20169  dvatan  20247  leibpi  20254  log2cnv  20256  efrlim  20280  cxp2lim  20287  cxploglim  20288  wilthlem1  20322  ftalem1  20326  ftalem5  20330  basellem3  20336  basellem5  20338  dvdsmulf1o  20450  sgmppw  20452  logfac2  20472  chpval2  20473  chpchtsum  20474  perfect1  20483  lgsdirprm  20584  lgsdi  20587  lgsdirnn0  20594  lgsdinn0  20595  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  lgsquad2  20615  2sqlem3  20621  2sqlem4  20622  chebbnd1lem2  20635  chebbnd1lem3  20636  chtppilimlem2  20639  chto1lb  20643  rplogsumlem1  20649  dchrisumlem2  20655  dchrvmasum2lem  20661  dchrisum0flblem2  20674  dchrisum0lem2a  20682  mulogsumlem  20696  mulog2sumlem2  20700  selberglem1  20710  selberg2lem  20715  selberg3lem1  20722  selberg4  20726  pntrsumo1  20730  selberg34r  20736  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntlemb  20762  pntlemq  20766  pntlemr  20767  pntlemj  20768  pntlemo  20772  pnt2  20778  pnt  20779  padicabvcxp  20797  ostth2lem2  20799  ostth2lem3  20800  ostth2lem4  20801  smcnlem  21286  pjhthlem1  21986  kbmul  22551  kbass2  22713  zetacvg  23704  subfacval2  23733  subfaclim  23734  faclimlem9  24125  brbtwn2  24605  colinearalglem1  24606  colinearalg  24610  axpaschlem  24640  axcontlem8  24671  bpoly4  24866  itg2addnclem  25003  itg2addnclem2  25004  itgabsnc  25020  ftc1cnnclem  25024  areacirclem2  25028  areacirc  25034  geomcau  26578  bfplem1  26649  rrndstprj2  26658  rrnequiv  26662  irrapxlem5  27014  pellexlem2  27018  pellexlem6  27022  qirropth  27096  rmxyadd  27109  rmxm1  27122  rmxluc  27124  rmyluc2  27126  rmydbl  27128  jm2.24nn  27149  jm2.17a  27150  jm2.17b  27151  jm2.17c  27152  jm2.18  27184  jm2.19lem2  27186  jm2.22  27191  jm2.23  27192  itgsinexplem1  27851  wallispilem4  27920  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem7  27932  stirlinglem10  27935  stirlinglem15  27940  sigarac  27945  sigarls  27950  sigarid  27951  sigardiv  27954  sigarcol  27957  sigaradd  27959  cevathlem1  27960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcom 8817
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator