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

Theorem mulcomd 10174
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 10135 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596  wcel 2103  (class class class)co 6765  cc 10047   · cmul 10054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10113
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  mul31  10317  subdir2d  10601  mulcand  10773  mulcan2d  10774  divcan1  10807  divrec2  10815  div23  10817  divdivdiv  10839  divmuleq  10843  divadddiv  10853  divcan5rd  10941  dmdcan2d  10944  mvllmuld  10970  subhalfhalf  11379  mul2lt0llt0  12048  mul2lt0lgt0  12049  xmulcom  12210  modvalr  12786  mulp1mod1  12826  modmul12d  12839  modnegd  12840  modmulmodr  12851  expaddz  13019  binom3  13100  expmulnbnd  13111  digit1  13113  bccmpl  13211  bcm1k  13217  bcn2  13221  bcpasc  13223  recval  14182  abs1m  14195  reccn2  14447  lo1mul2  14479  isummulc1  14614  fsummulc1  14637  incexclem  14688  incexc  14689  trireciplem  14714  geolim  14721  cvgrat  14735  mertens  14738  ntrivcvgmul  14754  fallfacfwd  14887  bpoly4  14910  fsumcube  14911  eftlub  14959  sinadd  15014  cosadd  15015  sin2t  15027  nndivides  15113  dvds2ln  15137  even2n  15189  oddm1even  15190  mod2eq1n2dvds  15194  m1exp1  15216  pwp1fsum  15237  divalgmod  15252  divalgmodOLD  15253  bitsp1  15276  bitsinv1lem  15286  sadadd2lem  15304  smumullem  15337  mulgcdr  15390  rplpwr  15399  lcmgcdlem  15442  divgcdcoprmex  15503  cncongr1  15504  eulerthlem2  15610  prmdiv  15613  prmdivdiv  15615  vfermltlALT  15630  modprmn0modprm0  15635  coprimeprodsq  15636  pythagtriplem6  15649  pythagtriplem7  15650  pceulem  15673  pcadd  15716  prmpwdvds  15731  mul4sqlem  15780  4sqlem17  15788  mulgassr  17702  odmodnn0  18080  odmulg  18094  odmulgeq  18095  odbezout  18096  odadd1  18372  ablfacrp2  18587  pgpfac1lem3  18597  zringlpirlem3  19957  znunit  20035  icopnfhmeo  22864  cphassr  23133  pjthlem1  23329  itgabs  23721  dvmulbr  23822  dvcmul  23827  dvcmulf  23828  dvmptcmul  23847  cmvth  23874  dvlipcn  23877  c1liplem1  23879  lhop1lem  23896  lhop2  23898  dvcvx  23903  dvfsumlem2  23910  ftc1lem4  23922  itgparts  23930  dvply1  24159  elqaalem3  24196  aalioulem4  24210  taylthlem2  24248  abelthlem6  24310  abelthlem7  24312  tangtx  24377  tanarg  24485  advlogexp  24521  mulcxp  24551  cxpmul  24554  abscxp  24558  dvcxp2  24602  cxpeq  24618  ang180lem1  24659  lawcoslem1  24665  lawcos  24666  heron  24685  dcubic1  24692  mcubic  24694  cubic2  24695  binom4  24697  dquart  24700  quart1lem  24702  quart1  24703  quartlem1  24704  dvatan  24782  leibpi  24789  log2cnv  24791  efrlim  24816  cxp2lim  24823  cxploglim  24824  zetacvg  24861  lgamgulmlem2  24876  lgamgulmlem3  24877  wilthlem1  24914  ftalem1  24919  ftalem5  24923  basellem3  24929  basellem5  24931  dvdsmulf1o  25040  sgmppw  25042  logfac2  25062  chpval2  25063  chpchtsum  25064  perfect1  25073  lgsdirprm  25176  lgsdi  25179  lgsdirnn0  25189  lgsdinn0  25190  gausslemma2dlem1a  25210  gausslemma2dlem6  25217  lgsquadlem1  25225  lgsquadlem2  25226  lgsquadlem3  25227  lgsquad2  25231  2lgslem3a1  25245  2lgslem3b1  25246  2lgslem3c1  25247  2lgslem3d1  25248  2lgsoddprmlem2  25254  2sqlem3  25265  2sqlem4  25266  chebbnd1lem2  25279  chebbnd1lem3  25280  chtppilimlem2  25283  chto1lb  25287  rplogsumlem1  25293  dchrisumlem2  25299  dchrvmasum2lem  25305  dchrisum0flblem2  25318  dchrisum0lem2a  25326  mulogsumlem  25340  mulog2sumlem2  25344  selberglem1  25354  selberg2lem  25359  selberg3lem1  25366  selberg4  25370  pntrsumo1  25374  selberg34r  25380  pntrlog2bndlem3  25388  pntrlog2bndlem4  25389  pntlemb  25406  pntlemq  25410  pntlemr  25411  pntlemj  25412  pntlemo  25416  pnt2  25422  pnt  25423  padicabvcxp  25441  ostth2lem2  25443  ostth2lem3  25444  ostth2lem4  25445  ttgcontlem1  25885  brbtwn2  25905  colinearalglem1  25906  colinearalg  25910  axpaschlem  25940  axcontlem8  25971  numclwwlk1  27441  numclwwlk7  27480  smcnlem  27782  pjhthlem1  28480  kbmul  29044  kbass2  29206  2sqmod  29878  psgnfzto1st  30085  qqhval2lem  30255  qqhghm  30262  qqhrhm  30263  oddpwdc  30646  sgnmul  30834  plymulx0  30854  signsvtp  30890  signsvtn  30891  signsvfpn  30892  signsvfnn  30893  breprexplemc  30940  circlemethhgt  30951  logdivsqrle  30958  hgt750lemf  30961  hgt750lemb  30964  hgt750leme  30966  subfacval2  31397  subfaclim  31398  fwddifnp1  32499  knoppndvlem11  32740  knoppndvlem17  32746  bj-subcom  33386  bj-rdiv  33388  bj-bary1lem1  33393  itg2addnclem  33693  itg2addnclem2  33694  itgabsnc  33711  ftc1cnnclem  33715  areacirclem1  33732  areacirc  33737  geomcau  33787  bfplem1  33853  rrndstprj2  33862  rrnequiv  33866  irrapxlem5  37809  pellexlem2  37813  pellexlem6  37817  qirropth  37892  rmxyadd  37905  rmxm1  37918  rmxluc  37920  rmyluc2  37922  rmydbl  37924  jm2.24nn  37945  jm2.17a  37946  jm2.17b  37947  jm2.17c  37948  jm2.18  37974  jm2.19lem2  37976  jm2.22  37981  jm2.23  37982  areaquad  38221  imo72b2  38894  int-mulcomd  38898  int-rightdistd  38902  cvgdvgrat  38931  radcnvrat  38932  bccm1k  38960  binomcxplemwb  38966  binomcxplemnotnn0  38974  sineq0ALT  39589  mul13d  39907  divdiv3d  39990  mccllem  40249  coskpi2  40497  cosknegpi  40500  dvsinax  40547  dvasinbx  40555  dvcosax  40561  dvnxpaek  40577  dvnmul  40578  dvnprodlem2  40582  itgsinexplem1  40589  stoweidlem1  40638  stoweidlem11  40648  stoweidlem26  40663  stoweidlem32  40669  wallispilem4  40705  wallispi2lem1  40708  wallispi2lem2  40709  stirlinglem3  40713  stirlinglem4  40714  stirlinglem5  40715  stirlinglem7  40717  stirlinglem10  40720  stirlinglem15  40725  dirkertrigeqlem1  40735  dirkertrigeqlem2  40736  dirkertrigeqlem3  40737  dirkertrigeq  40738  dirkercncflem1  40740  fourierdlem16  40760  fourierdlem21  40765  fourierdlem22  40766  fourierdlem56  40799  fourierdlem66  40809  fourierdlem83  40826  fourierswlem  40867  fouriersw  40868  etransclem23  40894  etransclem24  40895  etransclem38  40909  etransclem46  40917  hoiprodp1  41225  hoidmvlelem2  41233  smfmullem1  41421  sigarac  41464  sigarls  41469  sigarid  41470  sigardiv  41473  sigarcol  41476  sigaradd  41478  cevathlem1  41479  fmtnoodd  41872  sqrtpwpw2p  41877  fmtnorec3  41887  fmtnoprmfac2lem1  41905  fmtnofac1  41909  pwdif  41928  lighneallem2  41950  lighneallem3  41951  proththd  41958  dfeven2  41989  altgsumbc  42557  altgsumbcALT  42558  blennnt2  42810  dignn0flhalflem2  42837  dignn0ehalf  42838  amgmwlem  42978
  Copyright terms: Public domain W3C validator