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

Theorem mulcomd 9617
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 9578 . 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 1379    e. wcel 1767  (class class class)co 6284   CCcc 9490    x. cmul 9497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9556
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul31  9747  mulcand  10182  mulcan2d  10183  divcan1  10216  divrec2  10224  div23  10226  divdivdiv  10245  divmuleq  10249  divadddiv  10259  divcan5rd  10347  dmdcan2d  10350  mvllmuld  10376  xmulcom  11458  modvalr  11967  modmul12d  12009  modnegd  12010  expaddz  12178  binom3  12255  expmulnbnd  12266  digit1  12268  bccmpl  12355  bcm1k  12361  bcn2  12365  bcpasc  12367  recval  13118  abs1m  13131  reccn2  13382  lo1mul2  13414  isummulc1  13541  fsummulc1  13563  incexclem  13611  incexc  13612  trireciplem  13636  geolim  13642  cvgrat  13655  mertens  13658  eftlub  13705  sinadd  13760  cosadd  13761  sin2t  13773  dvds2ln  13875  oddm1even  13906  divalgmod  13923  bitsp1  13940  bitsinv1lem  13950  sadadd2lem  13968  smumullem  14001  mulgcdr  14045  rplpwr  14053  eulerthlem2  14171  prmdiv  14174  prmdivdiv  14176  modprmn0modprm0  14191  coprimeprodsq  14192  pythagtriplem6  14204  pythagtriplem7  14205  pceulem  14228  pcadd  14267  prmpwdvds  14281  mul4sqlem  14330  4sqlem17  14338  odmodnn0  16370  odmulg  16384  odmulgeq  16385  odbezout  16386  odadd1  16657  ablfacrp2  16920  pgpfac1lem3  16930  zringlpirlem3  18306  zlpirlem3  18311  znunit  18397  icopnfhmeo  21206  cphassr  21421  pjthlem1  21615  itgabs  22004  dvmulbr  22105  dvcmul  22110  dvcmulf  22111  dvmptcmul  22130  cmvth  22155  dvlipcn  22158  c1liplem1  22160  lhop1lem  22177  lhop2  22179  dvcvx  22184  dvfsumlem2  22191  ftc1lem4  22203  itgparts  22211  dvply1  22442  elqaalem3  22479  aalioulem4  22493  taylthlem2  22531  abelthlem6  22593  abelthlem7  22595  tangtx  22659  tanarg  22760  advlogexp  22792  mulcxp  22822  cxpmul  22825  abscxp  22829  dvcxp2  22873  cxpeq  22887  ang180lem1  22897  lawcoslem1  22903  lawcos  22904  heron  22925  dcubic1  22932  mcubic  22934  cubic2  22935  binom4  22937  dquart  22940  quart1lem  22942  quart1  22943  quartlem1  22944  dvatan  23022  leibpi  23029  log2cnv  23031  efrlim  23055  cxp2lim  23062  cxploglim  23063  wilthlem1  23098  ftalem1  23102  ftalem5  23106  basellem3  23112  basellem5  23114  dvdsmulf1o  23226  sgmppw  23228  logfac2  23248  chpval2  23249  chpchtsum  23250  perfect1  23259  lgsdirprm  23360  lgsdi  23363  lgsdirnn0  23370  lgsdinn0  23371  lgsquadlem1  23385  lgsquadlem2  23386  lgsquadlem3  23387  lgsquad2  23391  2sqlem3  23397  2sqlem4  23398  chebbnd1lem2  23411  chebbnd1lem3  23412  chtppilimlem2  23415  chto1lb  23419  rplogsumlem1  23425  dchrisumlem2  23431  dchrvmasum2lem  23437  dchrisum0flblem2  23450  dchrisum0lem2a  23458  mulogsumlem  23472  mulog2sumlem2  23476  selberglem1  23486  selberg2lem  23491  selberg3lem1  23498  selberg4  23502  pntrsumo1  23506  selberg34r  23512  pntrlog2bndlem3  23520  pntrlog2bndlem4  23521  pntlemb  23538  pntlemq  23542  pntlemr  23543  pntlemj  23544  pntlemo  23548  pnt2  23554  pnt  23555  padicabvcxp  23573  ostth2lem2  23575  ostth2lem3  23576  ostth2lem4  23577  ttgcontlem1  23892  brbtwn2  23912  colinearalglem1  23913  colinearalg  23917  axpaschlem  23947  axcontlem8  23978  numclwwlk1  24803  numclwwlk7  24819  smcnlem  25311  pjhthlem1  26013  kbmul  26578  kbass2  26740  mul2lt0llt0  27263  mul2lt0lgt0  27264  qqhval2lem  27626  qqhghm  27633  qqhrhm  27634  oddpwdc  27961  sgnmul  28149  plymulx0  28172  signsvtp  28208  signsvtn  28209  signsvfpn  28210  signsvfnn  28211  zetacvg  28225  lgamgulmlem2  28240  lgamgulmlem3  28241  subfacval2  28299  subfaclim  28300  ntrivcvgmul  28641  fallfacfwd  28763  bpoly4  29426  fsumcube  29427  itg2addnclem  29671  itg2addnclem2  29672  itgabsnc  29689  ftc1cnnclem  29693  areacirclem1  29712  areacirc  29717  geomcau  29883  bfplem1  29949  rrndstprj2  29958  rrnequiv  29962  irrapxlem5  30394  pellexlem2  30398  pellexlem6  30402  qirropth  30476  rmxyadd  30489  rmxm1  30502  rmxluc  30504  rmyluc2  30506  rmydbl  30508  jm2.24nn  30529  jm2.17a  30530  jm2.17b  30531  jm2.17c  30532  jm2.18  30562  jm2.19lem2  30564  jm2.22  30569  jm2.23  30570  areaquad  30817  lcmgcdlem  30840  mul13d  31066  coskpi2  31230  cosknegpi  31233  dvsinax  31269  dvasinbx  31278  dvcosax  31284  itgsinexplem1  31299  stoweidlem1  31329  stoweidlem11  31339  stoweidlem26  31354  stoweidlem32  31360  wallispilem4  31396  wallispi2lem1  31399  wallispi2lem2  31400  stirlinglem3  31404  stirlinglem4  31405  stirlinglem5  31406  stirlinglem7  31408  stirlinglem10  31411  stirlinglem15  31416  dirkertrigeqlem1  31426  dirkertrigeqlem2  31427  dirkertrigeqlem3  31428  dirkertrigeq  31429  dirkeritg  31430  dirkercncflem1  31431  fourierdlem16  31451  fourierdlem21  31456  fourierdlem22  31457  fourierdlem56  31491  fourierdlem66  31501  fourierdlem83  31518  fourierswlem  31559  fouriersw  31560  sigarac  31564  sigarls  31569  sigarid  31570  sigardiv  31573  sigarcol  31576  sigaradd  31578  cevathlem1  31579  altgsumbc  32037  altgsumbcALT  32038  sineq0ALT  32835  bj-subcom  33760  bj-rdiv  33765  bj-bary1lem  33769  bj-bary1lem1  33770
  Copyright terms: Public domain W3C validator