Theorem mulcomd 10651

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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		mulcom 10612	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   · cmul 10531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10590

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  mul31  10796  mul4r  10798  mulcand  11262  mulcan2d  11263  divcan1  11296  divrec2  11304  div23  11306  divdivdiv  11330  divmuleq  11334  divadddiv  11344  divcan5rd  11432  dmdcan2d  11435  mvllmuld  11461  rdiv  11464  subhalfhalf  11859  mul2lt0llt0  12481  mul2lt0lgt0  12482  prodge0ld  12485  xmulcom  12647  modvalr  13235  mulp1mod1  13275  modmul12d  13288  modnegd  13289  modmulmodr  13300  expaddz  13469  binom3  13581  expmulnbnd  13592  digit1  13594  bccmpl  13665  bcm1k  13671  bcn2  13675  bcpasc  13677  recval  14674  abs1m  14687  bhmafibid1cn  14815  bhmafibid2cn  14816  reccn2  14945  lo1mul2  14977  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  15717  pwp1fsum  15732  divalgmod  15747  bitsp1  15770  bitsinv1lem  15780  sadadd2lem  15798  smumullem  15831  gcdmultiplez  15873  mulgcdr  15888  rplpwr  15897  lcmgcdlem  15940  divgcdcoprmex  16000  cncongr1  16001  eulerthlem2  16109  prmdiv  16112  prmdivdiv  16114  vfermltlALT  16129  modprmn0modprm0  16134  coprimeprodsq  16135  pythagtriplem6  16148  pythagtriplem7  16149  pceulem  16172  pcadd  16215  prmpwdvds  16230  mul4sqlem  16279  4sqlem17  16287  mulgassr  18257  odmodnn0  18660  odmulg  18675  odmulgeq  18676  odbezout  18677  odadd1  18961  ablfacrp2  19182  pgpfac1lem3  19192  zringlpirlem3  20179  znunit  20255  icopnfhmeo  23548  cphassr  23817  pjthlem1  24041  itgabs  24438  dvmulbr  24542  dvcmul  24547  dvcmulf  24548  dvmptcmul  24567  cmvth  24594  dvlipcn  24597  c1liplem1  24599  lhop1lem  24616  lhop2  24618  dvcvx  24623  dvfsumlem2  24630  ftc1lem4  24642  itgparts  24650  dvply1  24880  elqaalem3  24917  aalioulem4  24931  taylthlem2  24969  abelthlem6  25031  abelthlem7  25033  tangtx  25098  tanarg  25210  advlogexp  25246  mulcxp  25276  cxpmul  25279  abscxp  25283  dvcxp2  25330  cxpeq  25346  ang180lem1  25395  lawcoslem1  25401  lawcos  25402  heron  25424  dcubic1  25431  mcubic  25433  cubic2  25434  binom4  25436  dquart  25439  quart1lem  25441  quart1  25442  quartlem1  25443  dvatan  25521  leibpi  25528  log2cnv  25530  efrlim  25555  cxp2lim  25562  cxploglim  25563  zetacvg  25600  lgamgulmlem2  25615  lgamgulmlem3  25616  wilthlem1  25653  ftalem1  25658  ftalem5  25662  basellem3  25668  basellem5  25670  dvdsmulf1o  25779  sgmppw  25781  logfac2  25801  chpval2  25802  chpchtsum  25803  perfect1  25812  lgsdirprm  25915  lgsdi  25918  lgsdirnn0  25928  lgsdinn0  25929  gausslemma2dlem1a  25949  gausslemma2dlem6  25956  lgsquadlem1  25964  lgsquadlem2  25965  lgsquadlem3  25966  lgsquad2  25970  2lgslem3a1  25984  2lgslem3b1  25985  2lgslem3c1  25986  2lgslem3d1  25987  2lgsoddprmlem2  25993  2sqlem3  26004  2sqlem4  26005  2sqmod  26020  chebbnd1lem2  26054  chebbnd1lem3  26055  chtppilimlem2  26058  chto1lb  26062  rplogsumlem1  26068  dchrisumlem2  26074  dchrvmasum2lem  26080  dchrisum0flblem2  26093  dchrisum0lem2a  26101  mulogsumlem  26115  mulog2sumlem2  26119  selberglem1  26129  selberg2lem  26134  selberg3lem1  26141  selberg4  26145  pntrsumo1  26149  selberg34r  26155  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntlemb  26181  pntlemq  26185  pntlemr  26186  pntlemj  26187  pntlemo  26191  pnt2  26197  pnt  26198  padicabvcxp  26216  ostth2lem2  26218  ostth2lem3  26219  ostth2lem4  26220  ttgcontlem1  26679  brbtwn2  26699  colinearalglem1  26700  colinearalg  26704  axpaschlem  26734  axcontlem8  26765  numclwwlk1  28146  numclwwlk7  28176  smcnlem  28480  pjhthlem1  29174  kbmul  29738  kbass2  29900  psgnfzto1st  30797  ccfldextdgrr  31145  qqhval2lem  31332  qqhghm  31339  qqhrhm  31340  oddpwdc  31722  sgnmul  31910  plymulx0  31927  signsvtp  31963  signsvtn  31964  signsvfpn  31965  signsvfnn  31966  breprexplemc  32013  circlemethhgt  32024  logdivsqrle  32031  hgt750lemf  32034  hgt750lemb  32037  hgt750leme  32039  subfacval2  32547  subfaclim  32548  fwddifnp1  33739  knoppndvlem11  33974  knoppndvlem17  33980  bj-subcom  34722  bj-bary1lem1  34725  itg2addnclem  35108  itg2addnclem2  35109  itgabsnc  35126  ftc1cnnclem  35128  areacirclem1  35145  areacirc  35150  geomcau  35197  bfplem1  35260  rrndstprj2  35269  rrnequiv  35273  lcmineqlem1  39317  lcmineqlem5  39321  lcmineqlem8  39324  lcmineqlem11  39327  lcmineqlem18  39334  lcmineqlem21  39337  2np3bcnp1  39348  2ap1caineq  39349  3cubeslem2  39626  3cubeslem3l  39627  3cubeslem3r  39628  irrapxlem5  39767  pellexlem2  39771  pellexlem6  39775  qirropth  39849  rmxyadd  39862  rmxm1  39875  rmxluc  39877  rmyluc2  39879  rmydbl  39881  jm2.24nn  39900  jm2.17a  39901  jm2.17b  39902  jm2.17c  39903  jm2.18  39929  jm2.19lem2  39931  jm2.22  39936  jm2.23  39937  areaquad  40166  imo72b2  40878  int-mulcomd  40882  int-rightdistd  40886  cvgdvgrat  41017  radcnvrat  41018  bccm1k  41046  binomcxplemwb  41052  binomcxplemnotnn0  41060  sineq0ALT  41643  mul13d  41910  divdiv3d  41991  mccllem  42239  coskpi2  42508  cosknegpi  42511  dvsinax  42555  dvasinbx  42562  dvcosax  42568  dvnxpaek  42584  dvnmul  42585  dvnprodlem2  42589  itgsinexplem1  42596  stoweidlem1  42643  stoweidlem11  42653  stoweidlem26  42668  stoweidlem32  42674  wallispilem4  42710  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem3  42718  stirlinglem4  42719  stirlinglem5  42720  stirlinglem7  42722  stirlinglem10  42725  stirlinglem15  42730  dirkertrigeqlem1  42740  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkercncflem1  42745  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem56  42804  fourierdlem66  42814  fourierdlem83  42831  fourierswlem  42872  fouriersw  42873  etransclem23  42899  etransclem24  42900  etransclem38  42914  etransclem46  42922  hoiprodp1  43227  hoidmvlelem2  43235  smfmullem1  43423  sigarac  43466  sigarls  43471  sigarid  43472  sigardiv  43475  sigarcol  43478  sigaradd  43480  cevathlem1  43481  sqrtnegnre  43864  fmtnoodd  44050  sqrtpwpw2p  44055  fmtnorec3  44065  fmtnoprmfac2lem1  44083  fmtnofac1  44087  lighneallem2  44124  lighneallem3  44125  proththd  44132  requad01  44139  dfeven2  44167  fppr2odd  44249  fpprwppr  44257  altgsumbc  44754  altgsumbcALT  44755  blennnt2  45003  dignn0flhalflem2  45030  dignn0ehalf  45031  itcovalt2lem2lem2  45088  affinecomb2  45117  rrx2linest  45156  itscnhlc0yqe  45173  itsclc0yqsollem1  45176  itscnhlc0xyqsol  45179  itschlc0xyqsol1  45180  itsclc0xyqsolr  45183  itsclquadb  45190  2itscplem3  45194  itscnhlinecirc02plem1  45196  itscnhlinecirc02plem2  45197  inlinecirc02p  45201  amgmwlem  45330