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

Theorem mulcomd 8856
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 8823 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  mul31  8980  mulcand  9401  mulcan2d  9402  divcan1  9433  divrec2  9441  div23  9443  divdivdiv  9461  divmuleq  9465  divadddiv  9475  divcan5rd  9563  dmdcan2d  9566  xmulcom  10586  modmul12d  11003  modnegd  11004  expaddz  11146  binom3  11222  expmulnbnd  11233  digit1  11235  bccmpl  11322  bcm1k  11327  bcp1nk  11329  bcn2  11331  bcpasc  11333  recval  11806  abs1m  11819  reccn2  12070  lo1mul2  12102  isummulc1  12226  fsummulc1  12247  incexclem  12295  incexc  12296  trireciplem  12320  geolim  12326  cvgrat  12339  mertens  12342  eftlub  12389  sinadd  12444  cosadd  12445  sin2t  12457  dvds2ln  12559  oddm1even  12588  divalgmod  12605  bitsp1  12622  bitsinv1lem  12632  sadadd2lem  12650  smumullem  12683  mulgcdr  12727  rplpwr  12735  eulerthlem2  12850  prmdiv  12853  prmdivdiv  12855  coprimeprodsq  12862  pythagtriplem6  12874  pythagtriplem7  12875  pceulem  12898  pcadd  12937  prmpwdvds  12951  mul4sqlem  13000  4sqlem17  13008  odmodnn0  14855  odmulg  14869  odmulgeq  14870  odbezout  14871  odadd1  15140  ablfacrp2  15302  pgpfac1lem3  15312  zlpirlem3  16443  znunit  16517  icopnfhmeo  18441  cphassr  18647  pjthlem1  18801  itgabs  19189  dvmulbr  19288  dvcmul  19293  dvcmulf  19294  dvcobr  19295  dvmptcmul  19313  cmvth  19338  dvlipcn  19341  c1liplem1  19343  lhop1lem  19360  lhop2  19362  dvcvx  19367  dvfsumlem2  19374  ftc1lem4  19386  itgparts  19394  dvply1  19664  elqaalem3  19701  aalioulem4  19715  taylthlem2  19753  abelthlem6  19812  abelthlem7  19814  tangtx  19873  tanarg  19970  advlogexp  20002  mulcxp  20032  cxpmul  20035  abscxp  20039  dvcxp2  20083  cxpeq  20097  ang180lem1  20107  lawcoslem1  20113  lawcos  20114  dcubic1  20141  mcubic  20143  cubic2  20144  binom4  20146  dquart  20149  quart1lem  20151  quart1  20152  quartlem1  20153  dvatan  20231  leibpi  20238  log2cnv  20240  efrlim  20264  cxp2lim  20271  cxploglim  20272  wilthlem1  20306  ftalem1  20310  ftalem5  20314  basellem3  20320  basellem5  20322  dvdsmulf1o  20434  sgmppw  20436  logfac2  20456  chpval2  20457  chpchtsum  20458  perfect1  20467  lgsdirprm  20568  lgsdi  20571  lgsdirnn0  20578  lgsdinn0  20579  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  lgsquad2  20599  2sqlem3  20605  2sqlem4  20606  chebbnd1lem2  20619  chebbnd1lem3  20620  chtppilimlem2  20623  chto1lb  20627  rplogsumlem1  20633  dchrisumlem2  20639  dchrvmasum2lem  20645  dchrisum0flblem2  20658  dchrisum0lem2a  20666  mulogsumlem  20680  mulog2sumlem2  20684  selberglem1  20694  selberg2lem  20699  selberg3lem1  20706  selberg4  20710  pntrsumo1  20714  selberg34r  20720  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntlemb  20746  pntlemq  20750  pntlemr  20751  pntlemj  20752  pntlemo  20756  pnt2  20762  pnt  20763  padicabvcxp  20781  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  smcnlem  21270  pjhthlem1  21970  kbmul  22535  kbass2  22697  zetacvg  23689  subfacval2  23718  subfaclim  23719  brbtwn2  24533  colinearalglem1  24534  colinearalg  24538  axpaschlem  24568  axcontlem8  24599  bpoly4  24794  areacirclem2  24925  areacirc  24931  geomcau  26475  bfplem1  26546  rrndstprj2  26555  rrnequiv  26559  irrapxlem5  26911  pellexlem2  26915  pellexlem6  26919  qirropth  26993  rmxyadd  27006  rmxm1  27019  rmxluc  27021  rmyluc2  27023  rmydbl  27025  jm2.24nn  27046  jm2.17a  27047  jm2.17b  27048  jm2.17c  27049  jm2.18  27081  jm2.19lem2  27083  jm2.22  27088  jm2.23  27089  itgsinexplem1  27748  wallispilem4  27817  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem7  27829  stirlinglem10  27832  stirlinglem15  27837  sigarac  27842  sigarls  27847  sigarid  27848  sigardiv  27851  sigarcol  27854  sigaradd  27856  cevathlem1  27857
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcom 8801
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator