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

Theorem mulcomd 10099
Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
mulcomd (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcomd
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 mulcom 10060 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 694 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972   · cmul 9979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10038
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  mul31  10242  subdir2d  10526  mulcand  10698  mulcan2d  10699  divcan1  10732  divrec2  10740  div23  10742  divdivdiv  10764  divmuleq  10768  divadddiv  10778  divcan5rd  10866  dmdcan2d  10869  mvllmuld  10895  subhalfhalf  11304  mul2lt0llt0  11972  mul2lt0lgt0  11973  xmulcom  12134  modvalr  12711  mulp1mod1  12751  modmul12d  12764  modnegd  12765  modmulmodr  12776  expaddz  12944  binom3  13025  expmulnbnd  13036  digit1  13038  bccmpl  13136  bcm1k  13142  bcn2  13146  bcpasc  13148  recval  14106  abs1m  14119  reccn2  14371  lo1mul2  14403  isummulc1  14538  fsummulc1  14561  incexclem  14612  incexc  14613  trireciplem  14638  geolim  14645  cvgrat  14659  mertens  14662  ntrivcvgmul  14678  fallfacfwd  14811  bpoly4  14834  fsumcube  14835  eftlub  14883  sinadd  14938  cosadd  14939  sin2t  14951  nndivides  15037  dvds2ln  15061  even2n  15113  oddm1even  15114  mod2eq1n2dvds  15118  m1exp1  15140  pwp1fsum  15161  divalgmod  15176  divalgmodOLD  15177  bitsp1  15200  bitsinv1lem  15210  sadadd2lem  15228  smumullem  15261  mulgcdr  15314  rplpwr  15323  lcmgcdlem  15366  divgcdcoprmex  15427  cncongr1  15428  eulerthlem2  15534  prmdiv  15537  prmdivdiv  15539  vfermltlALT  15554  modprmn0modprm0  15559  coprimeprodsq  15560  pythagtriplem6  15573  pythagtriplem7  15574  pceulem  15597  pcadd  15640  prmpwdvds  15655  mul4sqlem  15704  4sqlem17  15712  mulgassr  17627  odmodnn0  18005  odmulg  18019  odmulgeq  18020  odbezout  18021  odadd1  18297  ablfacrp2  18512  pgpfac1lem3  18522  zringlpirlem3  19882  znunit  19960  icopnfhmeo  22789  cphassr  23058  pjthlem1  23254  itgabs  23646  dvmulbr  23747  dvcmul  23752  dvcmulf  23753  dvmptcmul  23772  cmvth  23799  dvlipcn  23802  c1liplem1  23804  lhop1lem  23821  lhop2  23823  dvcvx  23828  dvfsumlem2  23835  ftc1lem4  23847  itgparts  23855  dvply1  24084  elqaalem3  24121  aalioulem4  24135  taylthlem2  24173  abelthlem6  24235  abelthlem7  24237  tangtx  24302  tanarg  24410  advlogexp  24446  mulcxp  24476  cxpmul  24479  abscxp  24483  dvcxp2  24527  cxpeq  24543  ang180lem1  24584  lawcoslem1  24590  lawcos  24591  heron  24610  dcubic1  24617  mcubic  24619  cubic2  24620  binom4  24622  dquart  24625  quart1lem  24627  quart1  24628  quartlem1  24629  dvatan  24707  leibpi  24714  log2cnv  24716  efrlim  24741  cxp2lim  24748  cxploglim  24749  zetacvg  24786  lgamgulmlem2  24801  lgamgulmlem3  24802  wilthlem1  24839  ftalem1  24844  ftalem5  24848  basellem3  24854  basellem5  24856  dvdsmulf1o  24965  sgmppw  24967  logfac2  24987  chpval2  24988  chpchtsum  24989  perfect1  24998  lgsdirprm  25101  lgsdi  25104  lgsdirnn0  25114  lgsdinn0  25115  gausslemma2dlem1a  25135  gausslemma2dlem6  25142  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  lgsquad2  25156  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgslem3d1  25173  2lgsoddprmlem2  25179  2sqlem3  25190  2sqlem4  25191  chebbnd1lem2  25204  chebbnd1lem3  25205  chtppilimlem2  25208  chto1lb  25212  rplogsumlem1  25218  dchrisumlem2  25224  dchrvmasum2lem  25230  dchrisum0flblem2  25243  dchrisum0lem2a  25251  mulogsumlem  25265  mulog2sumlem2  25269  selberglem1  25279  selberg2lem  25284  selberg3lem1  25291  selberg4  25295  pntrsumo1  25299  selberg34r  25305  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntlemb  25331  pntlemq  25335  pntlemr  25336  pntlemj  25337  pntlemo  25341  pnt2  25347  pnt  25348  padicabvcxp  25366  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  ttgcontlem1  25810  brbtwn2  25830  colinearalglem1  25831  colinearalg  25835  axpaschlem  25865  axcontlem8  25896  numclwwlk1  27351  numclwwlk7  27378  smcnlem  27680  pjhthlem1  28378  kbmul  28942  kbass2  29104  2sqmod  29776  psgnfzto1st  29983  qqhval2lem  30153  qqhghm  30160  qqhrhm  30161  oddpwdc  30544  sgnmul  30732  plymulx0  30752  signsvtp  30788  signsvtn  30789  signsvfpn  30790  signsvfnn  30791  breprexplemc  30838  circlemethhgt  30849  logdivsqrle  30856  hgt750lemf  30859  hgt750lemb  30862  hgt750leme  30864  subfacval2  31295  subfaclim  31296  fwddifnp1  32397  knoppndvlem11  32638  knoppndvlem17  32644  bj-subcom  33284  bj-rdiv  33286  bj-bary1lem1  33291  itg2addnclem  33591  itg2addnclem2  33592  itgabsnc  33609  ftc1cnnclem  33613  areacirclem1  33630  areacirc  33635  geomcau  33685  bfplem1  33751  rrndstprj2  33760  rrnequiv  33764  irrapxlem5  37707  pellexlem2  37711  pellexlem6  37715  qirropth  37790  rmxyadd  37803  rmxm1  37816  rmxluc  37818  rmyluc2  37820  rmydbl  37822  jm2.24nn  37843  jm2.17a  37844  jm2.17b  37845  jm2.17c  37846  jm2.18  37872  jm2.19lem2  37874  jm2.22  37879  jm2.23  37880  areaquad  38119  imo72b2  38792  int-mulcomd  38796  int-rightdistd  38800  cvgdvgrat  38829  radcnvrat  38830  bccm1k  38858  binomcxplemwb  38864  binomcxplemnotnn0  38872  sineq0ALT  39487  mul13d  39805  divdiv3d  39888  mccllem  40147  coskpi2  40395  cosknegpi  40398  dvsinax  40445  dvasinbx  40453  dvcosax  40459  dvnxpaek  40475  dvnmul  40476  dvnprodlem2  40480  itgsinexplem1  40487  stoweidlem1  40536  stoweidlem11  40546  stoweidlem26  40561  stoweidlem32  40567  wallispilem4  40603  wallispi2lem1  40606  wallispi2lem2  40607  stirlinglem3  40611  stirlinglem4  40612  stirlinglem5  40613  stirlinglem7  40615  stirlinglem10  40618  stirlinglem15  40623  dirkertrigeqlem1  40633  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem1  40638  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem56  40697  fourierdlem66  40707  fourierdlem83  40724  fourierswlem  40765  fouriersw  40766  etransclem23  40792  etransclem24  40793  etransclem38  40807  etransclem46  40815  hoiprodp1  41123  hoidmvlelem2  41131  smfmullem1  41319  sigarac  41362  sigarls  41367  sigarid  41368  sigardiv  41371  sigarcol  41374  sigaradd  41376  cevathlem1  41377  fmtnoodd  41770  sqrtpwpw2p  41775  fmtnorec3  41785  fmtnoprmfac2lem1  41803  fmtnofac1  41807  pwdif  41826  lighneallem2  41848  lighneallem3  41849  proththd  41856  dfeven2  41887  altgsumbc  42455  altgsumbcALT  42456  blennnt2  42708  dignn0flhalflem2  42735  dignn0ehalf  42736  amgmwlem  42876
  Copyright terms: Public domain W3C validator