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

Theorem mulcomd 10654
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 10615 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  (class class class)co 7151  cc 10527   · cmul 10534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10593
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  mul31  10799  mul4r  10801  mulcand  11265  mulcan2d  11266  divcan1  11299  divrec2  11307  div23  11309  divdivdiv  11333  divmuleq  11337  divadddiv  11347  divcan5rd  11435  dmdcan2d  11438  mvllmuld  11464  rdiv  11467  subhalfhalf  11863  mul2lt0llt0  12486  mul2lt0lgt0  12487  prodge0ld  12490  xmulcom  12652  modvalr  13233  mulp1mod1  13273  modmul12d  13286  modnegd  13287  modmulmodr  13298  expaddz  13466  binom3  13578  expmulnbnd  13589  digit1  13591  bccmpl  13662  bcm1k  13668  bcn2  13672  bcpasc  13674  recval  14675  abs1m  14688  bhmafibid1cn  14816  bhmafibid2cn  14817  reccn2  14946  lo1mul2  14978  isummulc1  15110  fsummulc1  15132  incexclem  15183  incexc  15184  trireciplem  15209  pwdif  15215  geolim  15218  cvgrat  15231  mertens  15234  ntrivcvgmul  15250  fallfacfwd  15382  bpoly4  15405  fsumcube  15406  eftlub  15454  sinadd  15509  cosadd  15510  sin2t  15522  nndivides  15609  dvds2ln  15634  even2n  15683  oddm1even  15684  mod2eq1n2dvds  15688  m1exp1  15719  pwp1fsum  15734  divalgmod  15749  bitsp1  15772  bitsinv1lem  15782  sadadd2lem  15800  smumullem  15833  gcdmultiplez  15875  mulgcdr  15890  rplpwr  15899  lcmgcdlem  15942  divgcdcoprmex  16002  cncongr1  16003  eulerthlem2  16111  prmdiv  16114  prmdivdiv  16116  vfermltlALT  16131  modprmn0modprm0  16136  coprimeprodsq  16137  pythagtriplem6  16150  pythagtriplem7  16151  pceulem  16174  pcadd  16217  prmpwdvds  16232  mul4sqlem  16281  4sqlem17  16289  mulgassr  18197  odmodnn0  18590  odmulg  18605  odmulgeq  18606  odbezout  18607  odadd1  18890  ablfacrp2  19111  pgpfac1lem3  19121  zringlpirlem3  20549  znunit  20626  icopnfhmeo  23462  cphassr  23731  pjthlem1  23955  itgabs  24350  dvmulbr  24451  dvcmul  24456  dvcmulf  24457  dvmptcmul  24476  cmvth  24503  dvlipcn  24506  c1liplem1  24508  lhop1lem  24525  lhop2  24527  dvcvx  24532  dvfsumlem2  24539  ftc1lem4  24551  itgparts  24559  dvply1  24788  elqaalem3  24825  aalioulem4  24839  taylthlem2  24877  abelthlem6  24939  abelthlem7  24941  tangtx  25006  tanarg  25115  advlogexp  25151  mulcxp  25181  cxpmul  25184  abscxp  25188  dvcxp2  25235  cxpeq  25251  ang180lem1  25300  lawcoslem1  25306  lawcos  25307  heron  25329  dcubic1  25336  mcubic  25338  cubic2  25339  binom4  25341  dquart  25344  quart1lem  25346  quart1  25347  quartlem1  25348  dvatan  25426  leibpi  25434  log2cnv  25436  efrlim  25461  cxp2lim  25468  cxploglim  25469  zetacvg  25506  lgamgulmlem2  25521  lgamgulmlem3  25522  wilthlem1  25559  ftalem1  25564  ftalem5  25568  basellem3  25574  basellem5  25576  dvdsmulf1o  25685  sgmppw  25687  logfac2  25707  chpval2  25708  chpchtsum  25709  perfect1  25718  lgsdirprm  25821  lgsdi  25824  lgsdirnn0  25834  lgsdinn0  25835  gausslemma2dlem1a  25855  gausslemma2dlem6  25862  lgsquadlem1  25870  lgsquadlem2  25871  lgsquadlem3  25872  lgsquad2  25876  2lgslem3a1  25890  2lgslem3b1  25891  2lgslem3c1  25892  2lgslem3d1  25893  2lgsoddprmlem2  25899  2sqlem3  25910  2sqlem4  25911  2sqmod  25926  chebbnd1lem2  25960  chebbnd1lem3  25961  chtppilimlem2  25964  chto1lb  25968  rplogsumlem1  25974  dchrisumlem2  25980  dchrvmasum2lem  25986  dchrisum0flblem2  25999  dchrisum0lem2a  26007  mulogsumlem  26021  mulog2sumlem2  26025  selberglem1  26035  selberg2lem  26040  selberg3lem1  26047  selberg4  26051  pntrsumo1  26055  selberg34r  26061  pntrlog2bndlem3  26069  pntrlog2bndlem4  26070  pntlemb  26087  pntlemq  26091  pntlemr  26092  pntlemj  26093  pntlemo  26097  pnt2  26103  pnt  26104  padicabvcxp  26122  ostth2lem2  26124  ostth2lem3  26125  ostth2lem4  26126  ttgcontlem1  26585  brbtwn2  26605  colinearalglem1  26606  colinearalg  26610  axpaschlem  26640  axcontlem8  26671  numclwwlk1  28054  numclwwlk7  28084  smcnlem  28388  pjhthlem1  29082  kbmul  29646  kbass2  29808  psgnfzto1st  30661  ccfldextdgrr  30943  qqhval2lem  31108  qqhghm  31115  qqhrhm  31116  oddpwdc  31498  sgnmul  31686  plymulx0  31703  signsvtp  31739  signsvtn  31740  signsvfpn  31741  signsvfnn  31742  breprexplemc  31789  circlemethhgt  31800  logdivsqrle  31807  hgt750lemf  31810  hgt750lemb  31813  hgt750leme  31815  subfacval2  32318  subfaclim  32319  fwddifnp1  33510  knoppndvlem11  33745  knoppndvlem17  33751  bj-subcom  34464  bj-bary1lem1  34467  itg2addnclem  34810  itg2addnclem2  34811  itgabsnc  34828  ftc1cnnclem  34832  areacirclem1  34849  areacirc  34854  geomcau  34902  bfplem1  34968  rrndstprj2  34977  rrnequiv  34981  3cubeslem2  39143  3cubeslem3l  39144  3cubeslem3r  39145  irrapxlem5  39284  pellexlem2  39288  pellexlem6  39292  qirropth  39366  rmxyadd  39379  rmxm1  39392  rmxluc  39394  rmyluc2  39396  rmydbl  39398  jm2.24nn  39417  jm2.17a  39418  jm2.17b  39419  jm2.17c  39420  jm2.18  39446  jm2.19lem2  39448  jm2.22  39453  jm2.23  39454  areaquad  39684  imo72b2  40387  int-mulcomd  40391  int-rightdistd  40395  cvgdvgrat  40506  radcnvrat  40507  bccm1k  40535  binomcxplemwb  40541  binomcxplemnotnn0  40549  sineq0ALT  41132  mul13d  41406  divdiv3d  41488  mccllem  41739  coskpi2  42008  cosknegpi  42011  dvsinax  42058  dvasinbx  42066  dvcosax  42072  dvnxpaek  42088  dvnmul  42089  dvnprodlem2  42093  itgsinexplem1  42100  stoweidlem1  42148  stoweidlem11  42158  stoweidlem26  42173  stoweidlem32  42179  wallispilem4  42215  wallispi2lem1  42218  wallispi2lem2  42219  stirlinglem3  42223  stirlinglem4  42224  stirlinglem5  42225  stirlinglem7  42227  stirlinglem10  42230  stirlinglem15  42235  dirkertrigeqlem1  42245  dirkertrigeqlem2  42246  dirkertrigeqlem3  42247  dirkertrigeq  42248  dirkercncflem1  42250  fourierdlem16  42270  fourierdlem21  42275  fourierdlem22  42276  fourierdlem56  42309  fourierdlem66  42319  fourierdlem83  42336  fourierswlem  42377  fouriersw  42378  etransclem23  42404  etransclem24  42405  etransclem38  42419  etransclem46  42427  hoiprodp1  42732  hoidmvlelem2  42740  smfmullem1  42928  sigarac  42971  sigarls  42976  sigarid  42977  sigardiv  42980  sigarcol  42983  sigaradd  42985  cevathlem1  42986  sqrtnegnre  43369  fmtnoodd  43523  sqrtpwpw2p  43528  fmtnorec3  43538  fmtnoprmfac2lem1  43556  fmtnofac1  43560  lighneallem2  43599  lighneallem3  43600  proththd  43607  requad01  43614  dfeven2  43642  fppr2odd  43724  fpprwppr  43732  altgsumbc  44228  altgsumbcALT  44229  blennnt2  44477  dignn0flhalflem2  44504  dignn0ehalf  44505  affinecomb2  44518  rrx2linest  44557  itscnhlc0yqe  44574  itsclc0yqsollem1  44577  itscnhlc0xyqsol  44580  itschlc0xyqsol1  44581  itsclc0xyqsolr  44584  itsclquadb  44591  2itscplem3  44595  itscnhlinecirc02plem1  44597  itscnhlinecirc02plem2  44598  inlinecirc02p  44602  amgmwlem  44731
  Copyright terms: Public domain W3C validator