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

Theorem mulcomd 9394
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 9355 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 654 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755  (class class class)co 6080   CCcc 9267    x. cmul 9274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9333
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul31  9524  mulcand  9956  mulcan2d  9957  divcan1  9990  divrec2  9998  div23  10000  divdivdiv  10019  divmuleq  10023  divadddiv  10033  divcan5rd  10121  dmdcan2d  10124  mvllmuld  10150  xmulcom  11216  modvalr  11694  modmul12d  11736  modnegd  11737  expaddz  11891  binom3  11968  expmulnbnd  11979  digit1  11981  bccmpl  12068  bcm1k  12074  bcn2  12078  bcpasc  12080  recval  12793  abs1m  12806  reccn2  13057  lo1mul2  13089  isummulc1  13213  fsummulc1  13234  incexclem  13281  incexc  13282  trireciplem  13306  geolim  13312  cvgrat  13325  mertens  13328  eftlub  13375  sinadd  13430  cosadd  13431  sin2t  13443  dvds2ln  13545  oddm1even  13575  divalgmod  13592  bitsp1  13609  bitsinv1lem  13619  sadadd2lem  13637  smumullem  13670  mulgcdr  13714  rplpwr  13722  eulerthlem2  13839  prmdiv  13842  prmdivdiv  13844  modprmn0modprm0  13857  coprimeprodsq  13858  pythagtriplem6  13870  pythagtriplem7  13871  pceulem  13894  pcadd  13933  prmpwdvds  13947  mul4sqlem  13996  4sqlem17  14004  odmodnn0  16022  odmulg  16036  odmulgeq  16037  odbezout  16038  odadd1  16309  ablfacrp2  16541  pgpfac1lem3  16551  zringlpirlem3  17746  zlpirlem3  17751  znunit  17837  icopnfhmeo  20356  cphassr  20571  pjthlem1  20765  itgabs  21153  dvmulbr  21254  dvcmul  21259  dvcmulf  21260  dvmptcmul  21279  cmvth  21304  dvlipcn  21307  c1liplem1  21309  lhop1lem  21326  lhop2  21328  dvcvx  21333  dvfsumlem2  21340  ftc1lem4  21352  itgparts  21360  dvply1  21634  elqaalem3  21671  aalioulem4  21685  taylthlem2  21723  abelthlem6  21785  abelthlem7  21787  tangtx  21851  tanarg  21952  advlogexp  21984  mulcxp  22014  cxpmul  22017  abscxp  22021  dvcxp2  22065  cxpeq  22079  ang180lem1  22089  lawcoslem1  22095  lawcos  22096  heron  22117  dcubic1  22124  mcubic  22126  cubic2  22127  binom4  22129  dquart  22132  quart1lem  22134  quart1  22135  quartlem1  22136  dvatan  22214  leibpi  22221  log2cnv  22223  efrlim  22247  cxp2lim  22254  cxploglim  22255  wilthlem1  22290  ftalem1  22294  ftalem5  22298  basellem3  22304  basellem5  22306  dvdsmulf1o  22418  sgmppw  22420  logfac2  22440  chpval2  22441  chpchtsum  22442  perfect1  22451  lgsdirprm  22552  lgsdi  22555  lgsdirnn0  22562  lgsdinn0  22563  lgsquadlem1  22577  lgsquadlem2  22578  lgsquadlem3  22579  lgsquad2  22583  2sqlem3  22589  2sqlem4  22590  chebbnd1lem2  22603  chebbnd1lem3  22604  chtppilimlem2  22607  chto1lb  22611  rplogsumlem1  22617  dchrisumlem2  22623  dchrvmasum2lem  22629  dchrisum0flblem2  22642  dchrisum0lem2a  22650  mulogsumlem  22664  mulog2sumlem2  22668  selberglem1  22678  selberg2lem  22683  selberg3lem1  22690  selberg4  22694  pntrsumo1  22698  selberg34r  22704  pntrlog2bndlem3  22712  pntrlog2bndlem4  22713  pntlemb  22730  pntlemq  22734  pntlemr  22735  pntlemj  22736  pntlemo  22740  pnt2  22746  pnt  22747  padicabvcxp  22765  ostth2lem2  22767  ostth2lem3  22768  ostth2lem4  22769  ttgcontlem1  22953  brbtwn2  22973  colinearalglem1  22974  colinearalg  22978  axpaschlem  23008  axcontlem8  23039  smcnlem  23914  pjhthlem1  24616  kbmul  25181  kbass2  25343  mul2lt0llt0  25864  mul2lt0lgt0  25865  qqhval2lem  26263  qqhghm  26270  qqhrhm  26271  oddpwdc  26584  sgnmul  26772  plymulx0  26795  signsvtp  26831  signsvtn  26832  signsvfpn  26833  signsvfnn  26834  zetacvg  26848  lgamgulmlem2  26863  lgamgulmlem3  26864  subfacval2  26922  subfaclim  26923  ntrivcvgmul  27263  fallfacfwd  27385  bpoly4  28048  fsumcube  28049  itg2addnclem  28284  itg2addnclem2  28285  itgabsnc  28302  ftc1cnnclem  28306  areacirclem1  28325  areacirc  28330  geomcau  28496  bfplem1  28562  rrndstprj2  28571  rrnequiv  28575  irrapxlem5  29009  pellexlem2  29013  pellexlem6  29017  qirropth  29091  rmxyadd  29104  rmxm1  29117  rmxluc  29119  rmyluc2  29121  rmydbl  29123  jm2.24nn  29144  jm2.17a  29145  jm2.17b  29146  jm2.17c  29147  jm2.18  29179  jm2.19lem2  29181  jm2.22  29186  jm2.23  29187  areaquad  29434  itgsinexplem1  29637  stoweidlem1  29639  stoweidlem11  29649  stoweidlem26  29664  stoweidlem32  29670  wallispilem4  29706  wallispi2lem1  29709  wallispi2lem2  29710  stirlinglem3  29714  stirlinglem4  29715  stirlinglem5  29716  stirlinglem7  29718  stirlinglem10  29721  stirlinglem15  29726  sigarac  29731  sigarls  29736  sigarid  29737  sigardiv  29740  sigarcol  29743  sigaradd  29745  cevathlem1  29746  numclwwlk1  30534  numclwwlk7  30550  sineq0ALT  31372  bj-subcom  32162  bj-rdiv  32167  bj-bary1lem  32171  bj-bary1lem1  32172
  Copyright terms: Public domain W3C validator