Theorem mulcomd 11265

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 11224	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	syl2anc 582	1 ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7417  ℂcc 11136   · cmul 11143

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

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  mul31  11411  mul4r  11413  mulcand  11877  mulcan2d  11878  divcan1  11911  divrec2  11919  div23  11921  divdivdiv  11945  divmuleq  11949  divadddiv  11959  divcan5rd  12047  dmdcan2d  12050  mvllmuld  12076  rdiv  12079  subhalfhalf  12476  mul2lt0llt0  13110  mul2lt0lgt0  13111  prodge0ld  13114  xmulcom  13277  modvalr  13869  mulp1mod1  13909  modmul12d  13922  modnegd  13923  modmulmodr  13934  expaddz  14103  binom3  14218  expmulnbnd  14229  digit1  14231  bccmpl  14300  bcm1k  14306  bcn2  14310  bcpasc  14312  recval  15301  abs1m  15314  bhmafibid1cn  15442  bhmafibid2cn  15443  reccn2  15573  lo1mul2  15605  isummulc1  15741  fsummulc1  15763  incexclem  15814  incexc  15815  trireciplem  15840  pwdif  15846  geolim  15848  cvgrat  15861  mertens  15864  ntrivcvgmul  15880  fallfacfwd  16012  bpoly4  16035  fsumcube  16036  eftlub  16085  sinadd  16140  cosadd  16141  sin2t  16153  nndivides  16240  dvds2ln  16265  even2n  16318  oddm1even  16319  mod2eq1n2dvds  16323  m1exp1  16352  pwp1fsum  16367  divalgmod  16382  bitsp1  16405  bitsinv1lem  16415  sadadd2lem  16433  smumullem  16466  gcdmultiplez  16510  mulgcdr  16525  rplpwr  16532  lcmgcdlem  16576  divgcdcoprmex  16636  cncongr1  16637  eulerthlem2  16750  prmdiv  16753  prmdivdiv  16755  vfermltlALT  16770  modprmn0modprm0  16775  coprimeprodsq  16776  pythagtriplem6  16789  pythagtriplem7  16790  pceulem  16813  pcadd  16857  prmpwdvds  16872  mul4sqlem  16921  4sqlem17  16929  mulgassr  19071  odmodnn0  19499  odmulg  19515  odmulgeq  19516  odbezout  19517  odadd1  19807  ablfacrp2  20028  pgpfac1lem3  20038  zringlpirlem3  21394  znunit  21501  icopnfhmeo  24898  cphassr  25170  pjthlem1  25395  itgabs  25794  dvmulbr  25899  dvmulbrOLD  25900  dvcmul  25905  dvcmulf  25906  dvmptcmul  25926  cmvth  25953  cmvthOLD  25954  dvlipcn  25957  c1liplem1  25959  lhop1lem  25976  lhop2  25978  dvcvx  25983  dvfsumlem2  25991  dvfsumlem2OLD  25992  ftc1lem4  26004  itgparts  26012  dvply1  26248  elqaalem3  26286  aalioulem4  26300  taylthlem2  26339  taylthlem2OLD  26340  abelthlem6  26403  abelthlem7  26405  tangtx  26470  tanarg  26583  advlogexp  26619  mulcxp  26649  cxpmul  26652  abscxp  26656  dvcxp2  26705  cxpeq  26722  ang180lem1  26771  lawcoslem1  26777  lawcos  26778  heron  26800  dcubic1  26807  mcubic  26809  cubic2  26810  binom4  26812  dquart  26815  quart1lem  26817  quart1  26818  quartlem1  26819  dvatan  26897  leibpi  26904  log2cnv  26906  efrlim  26931  efrlimOLD  26932  cxp2lim  26939  cxploglim  26940  zetacvg  26977  lgamgulmlem2  26992  lgamgulmlem3  26993  wilthlem1  27030  ftalem1  27035  ftalem5  27039  basellem3  27045  basellem5  27047  mpodvdsmulf1o  27156  dvdsmulf1o  27158  sgmppw  27160  logfac2  27180  chpval2  27181  chpchtsum  27182  perfect1  27191  lgsdirprm  27294  lgsdi  27297  lgsdirnn0  27307  lgsdinn0  27308  gausslemma2dlem1a  27328  gausslemma2dlem6  27335  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2  27349  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  2lgsoddprmlem2  27372  2sqlem3  27383  2sqlem4  27384  2sqmod  27399  chebbnd1lem2  27433  chebbnd1lem3  27434  chtppilimlem2  27437  chto1lb  27441  rplogsumlem1  27447  dchrisumlem2  27453  dchrvmasum2lem  27459  dchrisum0flblem2  27472  dchrisum0lem2a  27480  mulogsumlem  27494  mulog2sumlem2  27498  selberglem1  27508  selberg2lem  27513  selberg3lem1  27520  selberg4  27524  pntrsumo1  27528  selberg34r  27534  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntlemb  27560  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemo  27570  pnt2  27576  pnt  27577  padicabvcxp  27595  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  ttgcontlem1  28751  brbtwn2  28772  colinearalglem1  28773  colinearalg  28777  axpaschlem  28807  axcontlem8  28838  numclwwlk1  30227  numclwwlk7  30257  smcnlem  30563  pjhthlem1  31257  kbmul  31821  kbass2  31983  psgnfzto1st  32883  zringfrac  33314  ccfldextdgrr  33430  qqhval2lem  33652  qqhghm  33659  qqhrhm  33660  oddpwdc  34044  sgnmul  34232  plymulx0  34249  signsvtp  34285  signsvtn  34286  signsvfpn  34287  signsvfnn  34288  breprexplemc  34334  circlemethhgt  34345  logdivsqrle  34352  hgt750lemf  34355  hgt750lemb  34358  hgt750leme  34360  subfacval2  34867  subfaclim  34868  fwddifnp1  35831  knoppndvlem11  36067  knoppndvlem17  36073  bj-subcom  36857  bj-bary1lem1  36860  itg2addnclem  37214  itg2addnclem2  37215  itgabsnc  37232  ftc1cnnclem  37234  areacirclem1  37251  areacirc  37256  geomcau  37302  bfplem1  37365  rrndstprj2  37374  rrnequiv  37378  lcmineqlem1  41569  lcmineqlem5  41573  lcmineqlem8  41576  lcmineqlem11  41579  lcmineqlem18  41586  lcmineqlem21  41589  3lexlogpow5ineq2  41595  3lexlogpow2ineq1  41598  dvrelogpow2b  41608  aks4d1p1p7  41614  primrootscoprmpow  41639  primrootscoprbij  41642  aks6d1c1  41656  aks6d1c2  41670  2np3bcnp1  41685  2ap1caineq  41686  bcle2d  41720  aks6d1c7lem1  41721  nicomachus  41937  retire  41945  3cubeslem2  42170  3cubeslem3l  42171  3cubeslem3r  42172  irrapxlem5  42311  pellexlem2  42315  pellexlem6  42319  qirropth  42393  rmxyadd  42407  rmxm1  42420  rmxluc  42422  rmyluc2  42424  rmydbl  42426  jm2.24nn  42445  jm2.17a  42446  jm2.17b  42447  jm2.17c  42448  jm2.18  42474  jm2.19lem2  42476  jm2.22  42481  jm2.23  42482  areaquad  42709  imo72b2  43667  int-mulcomd  43671  int-rightdistd  43675  cvgdvgrat  43815  radcnvrat  43816  bccm1k  43844  binomcxplemwb  43850  binomcxplemnotnn0  43858  sineq0ALT  44441  mul13d  44724  divdiv3d  44804  mccllem  45048  coskpi2  45317  cosknegpi  45320  dvsinax  45364  dvasinbx  45371  dvcosax  45377  dvnxpaek  45393  dvnmul  45394  dvnprodlem2  45398  itgsinexplem1  45405  stoweidlem1  45452  stoweidlem11  45462  stoweidlem26  45477  stoweidlem32  45483  wallispilem4  45519  wallispi2lem1  45522  wallispi2lem2  45523  stirlinglem3  45527  stirlinglem4  45528  stirlinglem5  45529  stirlinglem7  45531  stirlinglem10  45534  stirlinglem15  45539  dirkertrigeqlem1  45549  dirkertrigeqlem2  45550  dirkertrigeqlem3  45551  dirkertrigeq  45552  dirkercncflem1  45554  fourierdlem16  45574  fourierdlem21  45579  fourierdlem22  45580  fourierdlem56  45613  fourierdlem66  45623  fourierdlem83  45640  fourierswlem  45681  fouriersw  45682  etransclem23  45708  etransclem24  45709  etransclem38  45723  etransclem46  45731  hoiprodp1  46039  hoidmvlelem2  46047  smfmullem1  46242  sigarac  46303  sigarls  46308  sigarid  46309  sigardiv  46312  sigarcol  46315  sigaradd  46317  cevathlem1  46318  sqrtnegnre  46750  fmtnoodd  46936  sqrtpwpw2p  46941  fmtnorec3  46951  fmtnoprmfac2lem1  46969  fmtnofac1  46973  lighneallem2  47009  lighneallem3  47010  proththd  47017  requad01  47024  dfeven2  47052  fppr2odd  47134  fpprwppr  47142  altgsumbc  47528  altgsumbcALT  47529  blennnt2  47774  dignn0flhalflem2  47801  dignn0ehalf  47802  itcovalt2lem2lem2  47859  affinecomb2  47888  rrx2linest  47927  itscnhlc0yqe  47944  itsclc0yqsollem1  47947  itscnhlc0xyqsol  47950  itschlc0xyqsol1  47951  itsclc0xyqsolr  47954  itsclquadb  47961  2itscplem3  47965  itscnhlinecirc02plem1  47967  itscnhlinecirc02plem2  47968  inlinecirc02p  47972  amgmwlem  48347