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

Theorem mulcomd 9606
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 9567 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    e. wcel 1823  (class class class)co 6270   CCcc 9479    x. cmul 9486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9545
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  mul31  9737  mulcand  10178  mulcan2d  10179  divcan1  10212  divrec2  10220  div23  10222  divdivdiv  10241  divmuleq  10245  divadddiv  10255  divcan5rd  10343  dmdcan2d  10346  mvllmuld  10372  xmulcom  11461  modvalr  11981  modmul12d  12023  modnegd  12024  expaddz  12192  binom3  12269  expmulnbnd  12280  digit1  12282  bccmpl  12369  bcm1k  12375  bcn2  12379  bcpasc  12381  recval  13237  abs1m  13250  reccn2  13501  lo1mul2  13533  isummulc1  13660  fsummulc1  13682  incexclem  13730  incexc  13731  trireciplem  13755  geolim  13761  cvgrat  13774  mertens  13777  ntrivcvgmul  13793  eftlub  13926  sinadd  13981  cosadd  13982  sin2t  13994  dvds2ln  14098  oddm1even  14131  divalgmod  14148  bitsp1  14165  bitsinv1lem  14175  sadadd2lem  14193  smumullem  14226  mulgcdr  14270  rplpwr  14278  eulerthlem2  14396  prmdiv  14399  prmdivdiv  14401  modprmn0modprm0  14416  coprimeprodsq  14417  pythagtriplem6  14429  pythagtriplem7  14430  pceulem  14453  pcadd  14492  prmpwdvds  14506  mul4sqlem  14555  4sqlem17  14563  odmodnn0  16763  odmulg  16777  odmulgeq  16778  odbezout  16779  odadd1  17053  ablfacrp2  17313  pgpfac1lem3  17323  zringlpirlem3  18699  znunit  18775  icopnfhmeo  21609  cphassr  21824  pjthlem1  22018  itgabs  22407  dvmulbr  22508  dvcmul  22513  dvcmulf  22514  dvmptcmul  22533  cmvth  22558  dvlipcn  22561  c1liplem1  22563  lhop1lem  22580  lhop2  22582  dvcvx  22587  dvfsumlem2  22594  ftc1lem4  22606  itgparts  22614  dvply1  22846  elqaalem3  22883  aalioulem4  22897  taylthlem2  22935  abelthlem6  22997  abelthlem7  22999  tangtx  23064  tanarg  23172  advlogexp  23204  mulcxp  23234  cxpmul  23237  abscxp  23241  dvcxp2  23285  cxpeq  23299  ang180lem1  23340  lawcoslem1  23346  lawcos  23347  heron  23366  dcubic1  23373  mcubic  23375  cubic2  23376  binom4  23378  dquart  23381  quart1lem  23383  quart1  23384  quartlem1  23385  dvatan  23463  leibpi  23470  log2cnv  23472  efrlim  23497  cxp2lim  23504  cxploglim  23505  wilthlem1  23540  ftalem1  23544  ftalem5  23548  basellem3  23554  basellem5  23556  dvdsmulf1o  23668  sgmppw  23670  logfac2  23690  chpval2  23691  chpchtsum  23692  perfect1  23701  lgsdirprm  23802  lgsdi  23805  lgsdirnn0  23812  lgsdinn0  23813  lgsquadlem1  23827  lgsquadlem2  23828  lgsquadlem3  23829  lgsquad2  23833  2sqlem3  23839  2sqlem4  23840  chebbnd1lem2  23853  chebbnd1lem3  23854  chtppilimlem2  23857  chto1lb  23861  rplogsumlem1  23867  dchrisumlem2  23873  dchrvmasum2lem  23879  dchrisum0flblem2  23892  dchrisum0lem2a  23900  mulogsumlem  23914  mulog2sumlem2  23918  selberglem1  23928  selberg2lem  23933  selberg3lem1  23940  selberg4  23944  pntrsumo1  23948  selberg34r  23954  pntrlog2bndlem3  23962  pntrlog2bndlem4  23963  pntlemb  23980  pntlemq  23984  pntlemr  23985  pntlemj  23986  pntlemo  23990  pnt2  23996  pnt  23997  padicabvcxp  24015  ostth2lem2  24017  ostth2lem3  24018  ostth2lem4  24019  ttgcontlem1  24390  brbtwn2  24410  colinearalglem1  24411  colinearalg  24415  axpaschlem  24445  axcontlem8  24476  numclwwlk1  25300  numclwwlk7  25316  smcnlem  25805  pjhthlem1  26507  kbmul  27072  kbass2  27234  mul2lt0llt0  27798  mul2lt0lgt0  27799  2sqmod  27870  qqhval2lem  28196  qqhghm  28203  qqhrhm  28204  oddpwdc  28557  sgnmul  28745  plymulx0  28768  signsvtp  28804  signsvtn  28805  signsvfpn  28806  signsvfnn  28807  zetacvg  28821  lgamgulmlem2  28836  lgamgulmlem3  28837  subfacval2  28895  subfaclim  28896  fallfacfwd  29399  bpoly4  30049  fsumcube  30050  itg2addnclem  30306  itg2addnclem2  30307  itgabsnc  30324  ftc1cnnclem  30328  areacirclem1  30347  areacirc  30352  geomcau  30492  bfplem1  30558  rrndstprj2  30567  rrnequiv  30571  irrapxlem5  31001  pellexlem2  31005  pellexlem6  31009  qirropth  31083  rmxyadd  31096  rmxm1  31109  rmxluc  31111  rmyluc2  31113  rmydbl  31115  jm2.24nn  31136  jm2.17a  31137  jm2.17b  31138  jm2.17c  31139  jm2.18  31169  jm2.19lem2  31171  jm2.22  31176  jm2.23  31177  areaquad  31425  cvgdvgrat  31435  radcnvrat  31436  lcmgcdlem  31453  bccm1k  31488  binomcxplemwb  31494  binomcxplemnotnn0  31502  mul13d  31701  subdir2d  31750  mccllem  31844  coskpi2  31905  cosknegpi  31908  dvsinax  31947  dvasinbx  31956  dvcosax  31962  dvnxpaek  31978  dvnmul  31979  dvnprodlem2  31983  itgsinexplem1  31991  stoweidlem1  32022  stoweidlem11  32032  stoweidlem26  32047  stoweidlem32  32053  wallispilem4  32089  wallispi2lem1  32092  wallispi2lem2  32093  stirlinglem3  32097  stirlinglem4  32098  stirlinglem5  32099  stirlinglem7  32101  stirlinglem10  32104  stirlinglem15  32109  dirkertrigeqlem1  32119  dirkertrigeqlem2  32120  dirkertrigeqlem3  32121  dirkertrigeq  32122  dirkercncflem1  32124  fourierdlem16  32144  fourierdlem21  32149  fourierdlem22  32150  fourierdlem56  32184  fourierdlem66  32194  fourierdlem83  32211  fourierswlem  32252  fouriersw  32253  etransclem23  32279  etransclem24  32280  etransclem38  32294  etransclem46  32302  sigarac  32308  sigarls  32313  sigarid  32314  sigardiv  32317  sigarcol  32320  sigaradd  32322  cevathlem1  32323  mod2eq1n2dvds  32534  dfeven2  32561  altgsumbc  33195  altgsumbcALT  33196  blennnt2  33464  dignn0flhalflem2  33491  dignn0ehalf  33492  sineq0ALT  34138  bj-subcom  35070  bj-rdiv  35072  bj-bary1lem1  35077  imo72b2  38445  int-mulcomd  38449  int-rightdistd  38453
  Copyright terms: Public domain W3C validator