Theorem mulcomd 10927

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

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

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

This theorem is referenced by:  mul31  11072  mul4r  11074  mulcand  11538  mulcan2d  11539  divcan1  11572  divrec2  11580  div23  11582  divdivdiv  11606  divmuleq  11610  divadddiv  11620  divcan5rd  11708  dmdcan2d  11711  mvllmuld  11737  rdiv  11740  subhalfhalf  12137  mul2lt0llt0  12763  mul2lt0lgt0  12764  prodge0ld  12767  xmulcom  12929  modvalr  13520  mulp1mod1  13560  modmul12d  13573  modnegd  13574  modmulmodr  13585  expaddz  13755  binom3  13867  expmulnbnd  13878  digit1  13880  bccmpl  13951  bcm1k  13957  bcn2  13961  bcpasc  13963  recval  14962  abs1m  14975  bhmafibid1cn  15103  bhmafibid2cn  15104  reccn2  15234  lo1mul2  15266  isummulc1  15403  fsummulc1  15425  incexclem  15476  incexc  15477  trireciplem  15502  pwdif  15508  geolim  15510  cvgrat  15523  mertens  15526  ntrivcvgmul  15542  fallfacfwd  15674  bpoly4  15697  fsumcube  15698  eftlub  15746  sinadd  15801  cosadd  15802  sin2t  15814  nndivides  15901  dvds2ln  15926  even2n  15979  oddm1even  15980  mod2eq1n2dvds  15984  m1exp1  16013  pwp1fsum  16028  divalgmod  16043  bitsp1  16066  bitsinv1lem  16076  sadadd2lem  16094  smumullem  16127  gcdmultiplez  16171  mulgcdr  16186  rplpwr  16195  lcmgcdlem  16239  divgcdcoprmex  16299  cncongr1  16300  eulerthlem2  16411  prmdiv  16414  prmdivdiv  16416  vfermltlALT  16431  modprmn0modprm0  16436  coprimeprodsq  16437  pythagtriplem6  16450  pythagtriplem7  16451  pceulem  16474  pcadd  16518  prmpwdvds  16533  mul4sqlem  16582  4sqlem17  16590  mulgassr  18656  odmodnn0  19063  odmulg  19078  odmulgeq  19079  odbezout  19080  odadd1  19364  ablfacrp2  19585  pgpfac1lem3  19595  zringlpirlem3  20598  znunit  20683  icopnfhmeo  24012  cphassr  24281  pjthlem1  24506  itgabs  24904  dvmulbr  25008  dvcmul  25013  dvcmulf  25014  dvmptcmul  25033  cmvth  25060  dvlipcn  25063  c1liplem1  25065  lhop1lem  25082  lhop2  25084  dvcvx  25089  dvfsumlem2  25096  ftc1lem4  25108  itgparts  25116  dvply1  25349  elqaalem3  25386  aalioulem4  25400  taylthlem2  25438  abelthlem6  25500  abelthlem7  25502  tangtx  25567  tanarg  25679  advlogexp  25715  mulcxp  25745  cxpmul  25748  abscxp  25752  dvcxp2  25799  cxpeq  25815  ang180lem1  25864  lawcoslem1  25870  lawcos  25871  heron  25893  dcubic1  25900  mcubic  25902  cubic2  25903  binom4  25905  dquart  25908  quart1lem  25910  quart1  25911  quartlem1  25912  dvatan  25990  leibpi  25997  log2cnv  25999  efrlim  26024  cxp2lim  26031  cxploglim  26032  zetacvg  26069  lgamgulmlem2  26084  lgamgulmlem3  26085  wilthlem1  26122  ftalem1  26127  ftalem5  26131  basellem3  26137  basellem5  26139  dvdsmulf1o  26248  sgmppw  26250  logfac2  26270  chpval2  26271  chpchtsum  26272  perfect1  26281  lgsdirprm  26384  lgsdi  26387  lgsdirnn0  26397  lgsdinn0  26398  gausslemma2dlem1a  26418  gausslemma2dlem6  26425  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  lgsquad2  26439  2lgslem3a1  26453  2lgslem3b1  26454  2lgslem3c1  26455  2lgslem3d1  26456  2lgsoddprmlem2  26462  2sqlem3  26473  2sqlem4  26474  2sqmod  26489  chebbnd1lem2  26523  chebbnd1lem3  26524  chtppilimlem2  26527  chto1lb  26531  rplogsumlem1  26537  dchrisumlem2  26543  dchrvmasum2lem  26549  dchrisum0flblem2  26562  dchrisum0lem2a  26570  mulogsumlem  26584  mulog2sumlem2  26588  selberglem1  26598  selberg2lem  26603  selberg3lem1  26610  selberg4  26614  pntrsumo1  26618  selberg34r  26624  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntlemb  26650  pntlemq  26654  pntlemr  26655  pntlemj  26656  pntlemo  26660  pnt2  26666  pnt  26667  padicabvcxp  26685  ostth2lem2  26687  ostth2lem3  26688  ostth2lem4  26689  ttgcontlem1  27155  brbtwn2  27176  colinearalglem1  27177  colinearalg  27181  axpaschlem  27211  axcontlem8  27242  numclwwlk1  28626  numclwwlk7  28656  smcnlem  28960  pjhthlem1  29654  kbmul  30218  kbass2  30380  psgnfzto1st  31274  ccfldextdgrr  31644  qqhval2lem  31831  qqhghm  31838  qqhrhm  31839  oddpwdc  32221  sgnmul  32409  plymulx0  32426  signsvtp  32462  signsvtn  32463  signsvfpn  32464  signsvfnn  32465  breprexplemc  32512  circlemethhgt  32523  logdivsqrle  32530  hgt750lemf  32533  hgt750lemb  32536  hgt750leme  32538  subfacval2  33049  subfaclim  33050  fwddifnp1  34394  knoppndvlem11  34629  knoppndvlem17  34635  bj-subcom  35406  bj-bary1lem1  35409  itg2addnclem  35755  itg2addnclem2  35756  itgabsnc  35773  ftc1cnnclem  35775  areacirclem1  35792  areacirc  35797  geomcau  35844  bfplem1  35907  rrndstprj2  35916  rrnequiv  35920  lcmineqlem1  39965  lcmineqlem5  39969  lcmineqlem8  39972  lcmineqlem11  39975  lcmineqlem18  39982  lcmineqlem21  39985  3lexlogpow5ineq2  39991  3lexlogpow2ineq1  39994  dvrelogpow2b  40004  aks4d1p1p7  40010  2np3bcnp1  40028  2ap1caineq  40029  3cubeslem2  40423  3cubeslem3l  40424  3cubeslem3r  40425  irrapxlem5  40564  pellexlem2  40568  pellexlem6  40572  qirropth  40646  rmxyadd  40659  rmxm1  40672  rmxluc  40674  rmyluc2  40676  rmydbl  40678  jm2.24nn  40697  jm2.17a  40698  jm2.17b  40699  jm2.17c  40700  jm2.18  40726  jm2.19lem2  40728  jm2.22  40733  jm2.23  40734  areaquad  40963  imo72b2  41672  int-mulcomd  41676  int-rightdistd  41680  cvgdvgrat  41820  radcnvrat  41821  bccm1k  41849  binomcxplemwb  41855  binomcxplemnotnn0  41863  sineq0ALT  42446  mul13d  42707  divdiv3d  42788  mccllem  43028  coskpi2  43297  cosknegpi  43300  dvsinax  43344  dvasinbx  43351  dvcosax  43357  dvnxpaek  43373  dvnmul  43374  dvnprodlem2  43378  itgsinexplem1  43385  stoweidlem1  43432  stoweidlem11  43442  stoweidlem26  43457  stoweidlem32  43463  wallispilem4  43499  wallispi2lem1  43502  wallispi2lem2  43503  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem7  43511  stirlinglem10  43514  stirlinglem15  43519  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem1  43534  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem56  43593  fourierdlem66  43603  fourierdlem83  43620  fourierswlem  43661  fouriersw  43662  etransclem23  43688  etransclem24  43689  etransclem38  43703  etransclem46  43711  hoiprodp1  44016  hoidmvlelem2  44024  smfmullem1  44212  sigarac  44255  sigarls  44260  sigarid  44261  sigardiv  44264  sigarcol  44267  sigaradd  44269  cevathlem1  44270  sqrtnegnre  44687  fmtnoodd  44873  sqrtpwpw2p  44878  fmtnorec3  44888  fmtnoprmfac2lem1  44906  fmtnofac1  44910  lighneallem2  44946  lighneallem3  44947  proththd  44954  requad01  44961  dfeven2  44989  fppr2odd  45071  fpprwppr  45079  altgsumbc  45576  altgsumbcALT  45577  blennnt2  45823  dignn0flhalflem2  45850  dignn0ehalf  45851  itcovalt2lem2lem2  45908  affinecomb2  45937  rrx2linest  45976  itscnhlc0yqe  45993  itsclc0yqsollem1  45996  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000  itsclc0xyqsolr  46003  itsclquadb  46010  2itscplem3  46014  itscnhlinecirc02plem1  46016  itscnhlinecirc02plem2  46017  inlinecirc02p  46021  amgmwlem  46392