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

Theorem mulcomd 9042
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 9009 . 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 1717  (class class class)co 6020   CCcc 8921    x. cmul 8928
This theorem is referenced by:  mul31  9166  mulcand  9587  mulcan2d  9588  divcan1  9619  divrec2  9627  div23  9629  divdivdiv  9647  divmuleq  9651  divadddiv  9661  divcan5rd  9749  dmdcan2d  9752  xmulcom  10777  modmul12d  11207  modnegd  11208  expaddz  11351  binom3  11427  expmulnbnd  11438  digit1  11440  bccmpl  11527  bcm1k  11533  bcn2  11537  bcpasc  11539  recval  12053  abs1m  12066  reccn2  12317  lo1mul2  12349  isummulc1  12474  fsummulc1  12495  incexclem  12543  incexc  12544  trireciplem  12568  geolim  12574  cvgrat  12587  mertens  12590  eftlub  12637  sinadd  12692  cosadd  12693  sin2t  12705  dvds2ln  12807  oddm1even  12836  divalgmod  12853  bitsp1  12870  bitsinv1lem  12880  sadadd2lem  12898  smumullem  12931  mulgcdr  12975  rplpwr  12983  eulerthlem2  13098  prmdiv  13101  prmdivdiv  13103  coprimeprodsq  13110  pythagtriplem6  13122  pythagtriplem7  13123  pceulem  13146  pcadd  13185  prmpwdvds  13199  mul4sqlem  13248  4sqlem17  13256  odmodnn0  15105  odmulg  15119  odmulgeq  15120  odbezout  15121  odadd1  15390  ablfacrp2  15552  pgpfac1lem3  15562  zlpirlem3  16693  znunit  16767  icopnfhmeo  18839  cphassr  19045  pjthlem1  19205  itgabs  19593  dvmulbr  19692  dvcmul  19697  dvcmulf  19698  dvmptcmul  19717  cmvth  19742  dvlipcn  19745  c1liplem1  19747  lhop1lem  19764  lhop2  19766  dvcvx  19771  dvfsumlem2  19778  ftc1lem4  19790  itgparts  19798  dvply1  20068  elqaalem3  20105  aalioulem4  20119  taylthlem2  20157  abelthlem6  20219  abelthlem7  20221  tangtx  20280  tanarg  20381  advlogexp  20413  mulcxp  20443  cxpmul  20446  abscxp  20450  dvcxp2  20494  cxpeq  20508  ang180lem1  20518  lawcoslem1  20524  lawcos  20525  dcubic1  20552  mcubic  20554  cubic2  20555  binom4  20557  dquart  20560  quart1lem  20562  quart1  20563  quartlem1  20564  dvatan  20642  leibpi  20649  log2cnv  20651  efrlim  20675  cxp2lim  20682  cxploglim  20683  wilthlem1  20718  ftalem1  20722  ftalem5  20726  basellem3  20732  basellem5  20734  dvdsmulf1o  20846  sgmppw  20848  logfac2  20868  chpval2  20869  chpchtsum  20870  perfect1  20879  lgsdirprm  20980  lgsdi  20983  lgsdirnn0  20990  lgsdinn0  20991  lgsquadlem1  21005  lgsquadlem2  21006  lgsquadlem3  21007  lgsquad2  21011  2sqlem3  21017  2sqlem4  21018  chebbnd1lem2  21031  chebbnd1lem3  21032  chtppilimlem2  21035  chto1lb  21039  rplogsumlem1  21045  dchrisumlem2  21051  dchrvmasum2lem  21057  dchrisum0flblem2  21070  dchrisum0lem2a  21078  mulogsumlem  21092  mulog2sumlem2  21096  selberglem1  21106  selberg2lem  21111  selberg3lem1  21118  selberg4  21122  pntrsumo1  21126  selberg34r  21132  pntrlog2bndlem3  21140  pntrlog2bndlem4  21141  pntlemb  21158  pntlemq  21162  pntlemr  21163  pntlemj  21164  pntlemo  21168  pnt2  21174  pnt  21175  padicabvcxp  21193  ostth2lem2  21195  ostth2lem3  21196  ostth2lem4  21197  smcnlem  22041  pjhthlem1  22741  kbmul  23306  kbass2  23468  qqhval2lem  24164  qqhghm  24171  qqhrhm  24172  zetacvg  24578  lgamgulmlem2  24593  lgamgulmlem3  24594  subfacval2  24652  subfaclim  24653  ntrivcvgmul  25009  fallfacfwd  25119  brbtwn2  25558  colinearalglem1  25559  colinearalg  25563  axpaschlem  25593  axcontlem8  25624  bpoly4  25819  fsumcube  25820  itg2addnclem  25957  itg2addnclem2  25958  itgabsnc  25974  ftc1cnnclem  25978  areacirclem2  25982  areacirc  25988  geomcau  26156  bfplem1  26222  rrndstprj2  26231  rrnequiv  26235  irrapxlem5  26580  pellexlem2  26584  pellexlem6  26588  qirropth  26662  rmxyadd  26675  rmxm1  26688  rmxluc  26690  rmyluc2  26692  rmydbl  26694  jm2.24nn  26715  jm2.17a  26716  jm2.17b  26717  jm2.17c  26718  jm2.18  26750  jm2.19lem2  26752  jm2.22  26757  jm2.23  26758  itgsinexplem1  27416  stoweidlem1  27418  stoweidlem11  27428  stoweidlem26  27443  stoweidlem32  27449  wallispilem4  27485  wallispi2lem1  27488  wallispi2lem2  27489  stirlinglem3  27493  stirlinglem4  27494  stirlinglem5  27495  stirlinglem7  27497  stirlinglem10  27500  stirlinglem15  27505  sigarac  27510  sigarls  27515  sigarid  27516  sigardiv  27519  sigarcol  27522  sigaradd  27524  cevathlem1  27525
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcom 8987
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator