Theorem mulcomd 11257

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7414  ℂcc 11128   · cmul 11135

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

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

This theorem is referenced by:  mul31  11403  mul4r  11405  mulcand  11869  mulcan2d  11870  divcan1  11903  divrec2  11911  div23  11913  divdivdiv  11937  divmuleq  11941  divadddiv  11951  divcan5rd  12039  dmdcan2d  12042  mvllmuld  12068  rdiv  12071  subhalfhalf  12468  mul2lt0llt0  13102  mul2lt0lgt0  13103  prodge0ld  13106  xmulcom  13269  modvalr  13861  mulp1mod1  13901  modmul12d  13914  modnegd  13915  modmulmodr  13926  expaddz  14095  binom3  14210  expmulnbnd  14221  digit1  14223  bccmpl  14292  bcm1k  14298  bcn2  14302  bcpasc  14304  recval  15293  abs1m  15306  bhmafibid1cn  15434  bhmafibid2cn  15435  reccn2  15565  lo1mul2  15597  isummulc1  15733  fsummulc1  15755  incexclem  15806  incexc  15807  trireciplem  15832  pwdif  15838  geolim  15840  cvgrat  15853  mertens  15856  ntrivcvgmul  15872  fallfacfwd  16004  bpoly4  16027  fsumcube  16028  eftlub  16077  sinadd  16132  cosadd  16133  sin2t  16145  nndivides  16232  dvds2ln  16257  even2n  16310  oddm1even  16311  mod2eq1n2dvds  16315  m1exp1  16344  pwp1fsum  16359  divalgmod  16374  bitsp1  16397  bitsinv1lem  16407  sadadd2lem  16425  smumullem  16458  gcdmultiplez  16502  mulgcdr  16517  rplpwr  16524  lcmgcdlem  16568  divgcdcoprmex  16628  cncongr1  16629  eulerthlem2  16742  prmdiv  16745  prmdivdiv  16747  vfermltlALT  16762  modprmn0modprm0  16767  coprimeprodsq  16768  pythagtriplem6  16781  pythagtriplem7  16782  pceulem  16805  pcadd  16849  prmpwdvds  16864  mul4sqlem  16913  4sqlem17  16921  mulgassr  19058  odmodnn0  19486  odmulg  19502  odmulgeq  19503  odbezout  19504  odadd1  19794  ablfacrp2  20015  pgpfac1lem3  20025  zringlpirlem3  21377  znunit  21484  icopnfhmeo  24855  cphassr  25127  pjthlem1  25352  itgabs  25751  dvmulbr  25856  dvmulbrOLD  25857  dvcmul  25862  dvcmulf  25863  dvmptcmul  25883  cmvth  25910  cmvthOLD  25911  dvlipcn  25914  c1liplem1  25916  lhop1lem  25933  lhop2  25935  dvcvx  25940  dvfsumlem2  25948  dvfsumlem2OLD  25949  ftc1lem4  25961  itgparts  25969  dvply1  26205  elqaalem3  26243  aalioulem4  26257  taylthlem2  26296  taylthlem2OLD  26297  abelthlem6  26360  abelthlem7  26362  tangtx  26427  tanarg  26540  advlogexp  26576  mulcxp  26606  cxpmul  26609  abscxp  26613  dvcxp2  26662  cxpeq  26679  ang180lem1  26728  lawcoslem1  26734  lawcos  26735  heron  26757  dcubic1  26764  mcubic  26766  cubic2  26767  binom4  26769  dquart  26772  quart1lem  26774  quart1  26775  quartlem1  26776  dvatan  26854  leibpi  26861  log2cnv  26863  efrlim  26888  efrlimOLD  26889  cxp2lim  26896  cxploglim  26897  zetacvg  26934  lgamgulmlem2  26949  lgamgulmlem3  26950  wilthlem1  26987  ftalem1  26992  ftalem5  26996  basellem3  27002  basellem5  27004  mpodvdsmulf1o  27113  dvdsmulf1o  27115  sgmppw  27117  logfac2  27137  chpval2  27138  chpchtsum  27139  perfect1  27148  lgsdirprm  27251  lgsdi  27254  lgsdirnn0  27264  lgsdinn0  27265  gausslemma2dlem1a  27285  gausslemma2dlem6  27292  lgsquadlem1  27300  lgsquadlem2  27301  lgsquadlem3  27302  lgsquad2  27306  2lgslem3a1  27320  2lgslem3b1  27321  2lgslem3c1  27322  2lgslem3d1  27323  2lgsoddprmlem2  27329  2sqlem3  27340  2sqlem4  27341  2sqmod  27356  chebbnd1lem2  27390  chebbnd1lem3  27391  chtppilimlem2  27394  chto1lb  27398  rplogsumlem1  27404  dchrisumlem2  27410  dchrvmasum2lem  27416  dchrisum0flblem2  27429  dchrisum0lem2a  27437  mulogsumlem  27451  mulog2sumlem2  27455  selberglem1  27465  selberg2lem  27470  selberg3lem1  27477  selberg4  27481  pntrsumo1  27485  selberg34r  27491  pntrlog2bndlem3  27499  pntrlog2bndlem4  27500  pntlemb  27517  pntlemq  27521  pntlemr  27522  pntlemj  27523  pntlemo  27527  pnt2  27533  pnt  27534  padicabvcxp  27552  ostth2lem2  27554  ostth2lem3  27555  ostth2lem4  27556  ttgcontlem1  28682  brbtwn2  28703  colinearalglem1  28704  colinearalg  28708  axpaschlem  28738  axcontlem8  28769  numclwwlk1  30158  numclwwlk7  30188  smcnlem  30494  pjhthlem1  31188  kbmul  31752  kbass2  31914  psgnfzto1st  32804  ccfldextdgrr  33292  qqhval2lem  33518  qqhghm  33525  qqhrhm  33526  oddpwdc  33910  sgnmul  34098  plymulx0  34115  signsvtp  34151  signsvtn  34152  signsvfpn  34153  signsvfnn  34154  breprexplemc  34200  circlemethhgt  34211  logdivsqrle  34218  hgt750lemf  34221  hgt750lemb  34224  hgt750leme  34226  subfacval2  34733  subfaclim  34734  fwddifnp1  35697  knoppndvlem11  35933  knoppndvlem17  35939  bj-subcom  36723  bj-bary1lem1  36726  itg2addnclem  37079  itg2addnclem2  37080  itgabsnc  37097  ftc1cnnclem  37099  areacirclem1  37116  areacirc  37121  geomcau  37167  bfplem1  37230  rrndstprj2  37239  rrnequiv  37243  lcmineqlem1  41437  lcmineqlem5  41441  lcmineqlem8  41444  lcmineqlem11  41447  lcmineqlem18  41454  lcmineqlem21  41457  3lexlogpow5ineq2  41463  3lexlogpow2ineq1  41466  dvrelogpow2b  41476  aks4d1p1p7  41482  primrootscoprmpow  41506  primrootscoprbij  41509  aks6d1c1  41520  aks6d1c2  41533  2np3bcnp1  41548  2ap1caineq  41549  nicomachus  41794  retire  41802  3cubeslem2  42027  3cubeslem3l  42028  3cubeslem3r  42029  irrapxlem5  42168  pellexlem2  42172  pellexlem6  42176  qirropth  42250  rmxyadd  42264  rmxm1  42277  rmxluc  42279  rmyluc2  42281  rmydbl  42283  jm2.24nn  42302  jm2.17a  42303  jm2.17b  42304  jm2.17c  42305  jm2.18  42331  jm2.19lem2  42333  jm2.22  42338  jm2.23  42339  areaquad  42567  imo72b2  43525  int-mulcomd  43529  int-rightdistd  43533  cvgdvgrat  43673  radcnvrat  43674  bccm1k  43702  binomcxplemwb  43708  binomcxplemnotnn0  43716  sineq0ALT  44299  mul13d  44584  divdiv3d  44664  mccllem  44908  coskpi2  45177  cosknegpi  45180  dvsinax  45224  dvasinbx  45231  dvcosax  45237  dvnxpaek  45253  dvnmul  45254  dvnprodlem2  45258  itgsinexplem1  45265  stoweidlem1  45312  stoweidlem11  45322  stoweidlem26  45337  stoweidlem32  45343  wallispilem4  45379  wallispi2lem1  45382  wallispi2lem2  45383  stirlinglem3  45387  stirlinglem4  45388  stirlinglem5  45389  stirlinglem7  45391  stirlinglem10  45394  stirlinglem15  45399  dirkertrigeqlem1  45409  dirkertrigeqlem2  45410  dirkertrigeqlem3  45411  dirkertrigeq  45412  dirkercncflem1  45414  fourierdlem16  45434  fourierdlem21  45439  fourierdlem22  45440  fourierdlem56  45473  fourierdlem66  45483  fourierdlem83  45500  fourierswlem  45541  fouriersw  45542  etransclem23  45568  etransclem24  45569  etransclem38  45583  etransclem46  45591  hoiprodp1  45899  hoidmvlelem2  45907  smfmullem1  46102  sigarac  46163  sigarls  46168  sigarid  46169  sigardiv  46172  sigarcol  46175  sigaradd  46177  cevathlem1  46178  sqrtnegnre  46610  fmtnoodd  46796  sqrtpwpw2p  46801  fmtnorec3  46811  fmtnoprmfac2lem1  46829  fmtnofac1  46833  lighneallem2  46869  lighneallem3  46870  proththd  46877  requad01  46884  dfeven2  46912  fppr2odd  46994  fpprwppr  47002  altgsumbc  47339  altgsumbcALT  47340  blennnt2  47585  dignn0flhalflem2  47612  dignn0ehalf  47613  itcovalt2lem2lem2  47670  affinecomb2  47699  rrx2linest  47738  itscnhlc0yqe  47755  itsclc0yqsollem1  47758  itscnhlc0xyqsol  47761  itschlc0xyqsol1  47762  itsclc0xyqsolr  47765  itsclquadb  47772  2itscplem3  47776  itscnhlinecirc02plem1  47778  itscnhlinecirc02plem2  47779  inlinecirc02p  47783  amgmwlem  48158