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

Theorem mulcomd 9101
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 9068 . 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 1652    e. wcel 1725  (class class class)co 6073   CCcc 8980    x. cmul 8987
This theorem is referenced by:  mul31  9226  mulcand  9647  mulcan2d  9648  divcan1  9679  divrec2  9687  div23  9689  divdivdiv  9707  divmuleq  9711  divadddiv  9721  divcan5rd  9809  dmdcan2d  9812  xmulcom  10837  modmul12d  11272  modnegd  11273  expaddz  11416  binom3  11492  expmulnbnd  11503  digit1  11505  bccmpl  11592  bcm1k  11598  bcn2  11602  bcpasc  11604  recval  12118  abs1m  12131  reccn2  12382  lo1mul2  12414  isummulc1  12539  fsummulc1  12560  incexclem  12608  incexc  12609  trireciplem  12633  geolim  12639  cvgrat  12652  mertens  12655  eftlub  12702  sinadd  12757  cosadd  12758  sin2t  12770  dvds2ln  12872  oddm1even  12901  divalgmod  12918  bitsp1  12935  bitsinv1lem  12945  sadadd2lem  12963  smumullem  12996  mulgcdr  13040  rplpwr  13048  eulerthlem2  13163  prmdiv  13166  prmdivdiv  13168  coprimeprodsq  13175  pythagtriplem6  13187  pythagtriplem7  13188  pceulem  13211  pcadd  13250  prmpwdvds  13264  mul4sqlem  13313  4sqlem17  13321  odmodnn0  15170  odmulg  15184  odmulgeq  15185  odbezout  15186  odadd1  15455  ablfacrp2  15617  pgpfac1lem3  15627  zlpirlem3  16762  znunit  16836  icopnfhmeo  18960  cphassr  19166  pjthlem1  19330  itgabs  19718  dvmulbr  19817  dvcmul  19822  dvcmulf  19823  dvmptcmul  19842  cmvth  19867  dvlipcn  19870  c1liplem1  19872  lhop1lem  19889  lhop2  19891  dvcvx  19896  dvfsumlem2  19903  ftc1lem4  19915  itgparts  19923  dvply1  20193  elqaalem3  20230  aalioulem4  20244  taylthlem2  20282  abelthlem6  20344  abelthlem7  20346  tangtx  20405  tanarg  20506  advlogexp  20538  mulcxp  20568  cxpmul  20571  abscxp  20575  dvcxp2  20619  cxpeq  20633  ang180lem1  20643  lawcoslem1  20649  lawcos  20650  dcubic1  20677  mcubic  20679  cubic2  20680  binom4  20682  dquart  20685  quart1lem  20687  quart1  20688  quartlem1  20689  dvatan  20767  leibpi  20774  log2cnv  20776  efrlim  20800  cxp2lim  20807  cxploglim  20808  wilthlem1  20843  ftalem1  20847  ftalem5  20851  basellem3  20857  basellem5  20859  dvdsmulf1o  20971  sgmppw  20973  logfac2  20993  chpval2  20994  chpchtsum  20995  perfect1  21004  lgsdirprm  21105  lgsdi  21108  lgsdirnn0  21115  lgsdinn0  21116  lgsquadlem1  21130  lgsquadlem2  21131  lgsquadlem3  21132  lgsquad2  21136  2sqlem3  21142  2sqlem4  21143  chebbnd1lem2  21156  chebbnd1lem3  21157  chtppilimlem2  21160  chto1lb  21164  rplogsumlem1  21170  dchrisumlem2  21176  dchrvmasum2lem  21182  dchrisum0flblem2  21195  dchrisum0lem2a  21203  mulogsumlem  21217  mulog2sumlem2  21221  selberglem1  21231  selberg2lem  21236  selberg3lem1  21243  selberg4  21247  pntrsumo1  21251  selberg34r  21257  pntrlog2bndlem3  21265  pntrlog2bndlem4  21266  pntlemb  21283  pntlemq  21287  pntlemr  21288  pntlemj  21289  pntlemo  21293  pnt2  21299  pnt  21300  padicabvcxp  21318  ostth2lem2  21320  ostth2lem3  21321  ostth2lem4  21322  smcnlem  22185  pjhthlem1  22885  kbmul  23450  kbass2  23612  qqhval2lem  24357  qqhghm  24364  qqhrhm  24365  zetacvg  24791  lgamgulmlem2  24806  lgamgulmlem3  24807  subfacval2  24865  subfaclim  24866  ntrivcvgmul  25222  fallfacfwd  25344  brbtwn2  25836  colinearalglem1  25837  colinearalg  25841  axpaschlem  25871  axcontlem8  25902  bpoly4  26097  fsumcube  26098  itg2addnclem  26246  itg2addnclem2  26247  itgabsnc  26264  ftc1cnnclem  26268  areacirclem2  26282  areacirc  26288  geomcau  26456  bfplem1  26522  rrndstprj2  26531  rrnequiv  26535  irrapxlem5  26880  pellexlem2  26884  pellexlem6  26888  qirropth  26962  rmxyadd  26975  rmxm1  26988  rmxluc  26990  rmyluc2  26992  rmydbl  26994  jm2.24nn  27015  jm2.17a  27016  jm2.17b  27017  jm2.17c  27018  jm2.18  27050  jm2.19lem2  27052  jm2.22  27057  jm2.23  27058  itgsinexplem1  27715  stoweidlem1  27717  stoweidlem11  27727  stoweidlem26  27742  stoweidlem32  27748  wallispilem4  27784  wallispi2lem1  27787  wallispi2lem2  27788  stirlinglem3  27792  stirlinglem4  27793  stirlinglem5  27794  stirlinglem7  27796  stirlinglem10  27799  stirlinglem15  27804  sigarac  27809  sigarls  27814  sigarid  27815  sigardiv  27818  sigarcol  27821  sigaradd  27823  cevathlem1  27824  modvalr  28127  sineq0ALT  28986
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcom 9046
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator