Theorem mulcomd 11311

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

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

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

This theorem is referenced by:  mul31  11457  mul4r  11459  mulcand  11923  mulcan2d  11924  divcan1  11958  divrec2  11966  div23  11968  divdivdiv  11995  divmuleq  11999  divadddiv  12009  divcan5rd  12097  dmdcan2d  12100  mvllmuld  12126  rdiv  12129  subhalfhalf  12527  mul2lt0llt0  13161  mul2lt0lgt0  13162  prodge0ld  13165  xmulcom  13328  modvalr  13923  mulp1mod1  13963  modmul12d  13976  modnegd  13977  modmulmodr  13988  expaddz  14157  binom3  14273  expmulnbnd  14284  digit1  14286  bccmpl  14358  bcm1k  14364  bcn2  14368  bcpasc  14370  recval  15371  abs1m  15384  bhmafibid1cn  15512  bhmafibid2cn  15513  reccn2  15643  lo1mul2  15675  isummulc1  15811  fsummulc1  15833  incexclem  15884  incexc  15885  trireciplem  15910  pwdif  15916  geolim  15918  cvgrat  15931  mertens  15934  ntrivcvgmul  15950  fallfacfwd  16084  bpoly4  16107  fsumcube  16108  eftlub  16157  sinadd  16212  cosadd  16213  sin2t  16225  nndivides  16312  dvds2ln  16337  even2n  16390  oddm1even  16391  mod2eq1n2dvds  16395  m1exp1  16424  pwp1fsum  16439  divalgmod  16454  bitsp1  16477  bitsinv1lem  16487  sadadd2lem  16505  smumullem  16538  gcdmultiplez  16582  mulgcdr  16597  rplpwr  16605  lcmgcdlem  16653  divgcdcoprmex  16713  cncongr1  16714  eulerthlem2  16829  prmdiv  16832  prmdivdiv  16834  vfermltlALT  16849  modprmn0modprm0  16854  coprimeprodsq  16855  pythagtriplem6  16868  pythagtriplem7  16869  pceulem  16892  pcadd  16936  prmpwdvds  16951  mul4sqlem  17000  4sqlem17  17008  mulgassr  19152  odmodnn0  19582  odmulg  19598  odmulgeq  19599  odbezout  19600  odadd1  19890  ablfacrp2  20111  pgpfac1lem3  20121  zringlpirlem3  21498  znunit  21605  icopnfhmeo  24993  cphassr  25265  pjthlem1  25490  itgabs  25890  dvmulbr  25995  dvmulbrOLD  25996  dvcmul  26001  dvcmulf  26002  dvmptcmul  26022  cmvth  26049  cmvthOLD  26050  dvlipcn  26053  c1liplem1  26055  lhop1lem  26072  lhop2  26074  dvcvx  26079  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc1lem4  26100  itgparts  26108  dvply1  26343  elqaalem3  26381  aalioulem4  26395  taylthlem2  26434  taylthlem2OLD  26435  abelthlem6  26498  abelthlem7  26500  tangtx  26565  tanarg  26679  advlogexp  26715  mulcxp  26745  cxpmul  26748  abscxp  26752  dvcxp2  26801  cxpeq  26818  ang180lem1  26870  lawcoslem1  26876  lawcos  26877  heron  26899  dcubic1  26906  mcubic  26908  cubic2  26909  binom4  26911  dquart  26914  quart1lem  26916  quart1  26917  quartlem1  26918  dvatan  26996  leibpi  27003  log2cnv  27005  efrlim  27030  efrlimOLD  27031  cxp2lim  27038  cxploglim  27039  zetacvg  27076  lgamgulmlem2  27091  lgamgulmlem3  27092  wilthlem1  27129  ftalem1  27134  ftalem5  27138  basellem3  27144  basellem5  27146  mpodvdsmulf1o  27255  dvdsmulf1o  27257  sgmppw  27259  logfac2  27279  chpval2  27280  chpchtsum  27281  perfect1  27290  lgsdirprm  27393  lgsdi  27396  lgsdirnn0  27406  lgsdinn0  27407  gausslemma2dlem1a  27427  gausslemma2dlem6  27434  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad2  27448  2lgslem3a1  27462  2lgslem3b1  27463  2lgslem3c1  27464  2lgslem3d1  27465  2lgsoddprmlem2  27471  2sqlem3  27482  2sqlem4  27483  2sqmod  27498  chebbnd1lem2  27532  chebbnd1lem3  27533  chtppilimlem2  27536  chto1lb  27540  rplogsumlem1  27546  dchrisumlem2  27552  dchrvmasum2lem  27558  dchrisum0flblem2  27571  dchrisum0lem2a  27579  mulogsumlem  27593  mulog2sumlem2  27597  selberglem1  27607  selberg2lem  27612  selberg3lem1  27619  selberg4  27623  pntrsumo1  27627  selberg34r  27633  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntlemb  27659  pntlemq  27663  pntlemr  27664  pntlemj  27665  pntlemo  27669  pnt2  27675  pnt  27676  padicabvcxp  27694  ostth2lem2  27696  ostth2lem3  27697  ostth2lem4  27698  ttgcontlem1  28917  brbtwn2  28938  colinearalglem1  28939  colinearalg  28943  axpaschlem  28973  axcontlem8  29004  numclwwlk1  30393  numclwwlk7  30423  smcnlem  30729  pjhthlem1  31423  kbmul  31987  kbass2  32149  submuladdd  32753  muldivdid  32754  quad3d  32757  psgnfzto1st  33098  zringfrac  33547  ccfldextdgrr  33682  fldext2chn  33719  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  qqhval2lem  33927  qqhghm  33934  qqhrhm  33935  oddpwdc  34319  sgnmul  34507  plymulx0  34524  signsvtp  34560  signsvtn  34561  signsvfpn  34562  signsvfnn  34563  breprexplemc  34609  circlemethhgt  34620  logdivsqrle  34627  hgt750lemf  34630  hgt750lemb  34633  hgt750leme  34635  subfacval2  35155  subfaclim  35156  fwddifnp1  36129  knoppndvlem11  36488  knoppndvlem17  36494  bj-subcom  37274  bj-bary1lem1  37277  itg2addnclem  37631  itg2addnclem2  37632  itgabsnc  37649  ftc1cnnclem  37651  areacirclem1  37668  areacirc  37673  geomcau  37719  bfplem1  37782  rrndstprj2  37791  rrnequiv  37795  lcmineqlem1  41986  lcmineqlem5  41990  lcmineqlem8  41993  lcmineqlem11  41996  lcmineqlem18  42003  lcmineqlem21  42006  3lexlogpow5ineq2  42012  3lexlogpow2ineq1  42015  dvrelogpow2b  42025  aks4d1p1p7  42031  primrootscoprmpow  42056  primrootscoprbij  42059  aks6d1c1  42073  aks6d1c2  42087  2np3bcnp1  42101  2ap1caineq  42102  bcle2d  42136  aks6d1c7lem1  42137  nicomachus  42300  retire  42308  3cubeslem2  42641  3cubeslem3l  42642  3cubeslem3r  42643  irrapxlem5  42782  pellexlem2  42786  pellexlem6  42790  qirropth  42864  rmxyadd  42878  rmxm1  42891  rmxluc  42893  rmyluc2  42895  rmydbl  42897  jm2.24nn  42916  jm2.17a  42917  jm2.17b  42918  jm2.17c  42919  jm2.18  42945  jm2.19lem2  42947  jm2.22  42952  jm2.23  42953  areaquad  43177  imo72b2  44134  int-mulcomd  44138  int-rightdistd  44142  cvgdvgrat  44282  radcnvrat  44283  bccm1k  44311  binomcxplemwb  44317  binomcxplemnotnn0  44325  sineq0ALT  44908  mul13d  45194  divdiv3d  45274  mccllem  45518  coskpi2  45787  cosknegpi  45790  dvsinax  45834  dvasinbx  45841  dvcosax  45847  dvnxpaek  45863  dvnmul  45864  dvnprodlem2  45868  itgsinexplem1  45875  stoweidlem1  45922  stoweidlem11  45932  stoweidlem26  45947  stoweidlem32  45953  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem7  46001  stirlinglem10  46004  stirlinglem15  46009  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem1  46024  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem56  46083  fourierdlem66  46093  fourierdlem83  46110  fourierswlem  46151  fouriersw  46152  etransclem23  46178  etransclem24  46179  etransclem38  46193  etransclem46  46201  hoiprodp1  46509  hoidmvlelem2  46517  smfmullem1  46712  sigarac  46773  sigarls  46778  sigarid  46779  sigardiv  46782  sigarcol  46785  sigaradd  46787  cevathlem1  46788  sqrtnegnre  47222  fmtnoodd  47407  sqrtpwpw2p  47412  fmtnorec3  47422  fmtnoprmfac2lem1  47440  fmtnofac1  47444  lighneallem2  47480  lighneallem3  47481  proththd  47488  requad01  47495  dfeven2  47523  fppr2odd  47605  fpprwppr  47613  altgsumbc  48077  altgsumbcALT  48078  blennnt2  48323  dignn0flhalflem2  48350  dignn0ehalf  48351  itcovalt2lem2lem2  48408  affinecomb2  48437  rrx2linest  48476  itscnhlc0yqe  48493  itsclc0yqsollem1  48496  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500  itsclc0xyqsolr  48503  itsclquadb  48510  2itscplem3  48514  itscnhlinecirc02plem1  48516  itscnhlinecirc02plem2  48517  inlinecirc02p  48521  amgmwlem  48896