Theorem mulcomd 11155

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

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

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

This theorem is referenced by:  mul31  11301  mul4r  11303  mulcand  11771  mulcan2d  11772  divcan1  11806  divrec2  11814  div23  11816  divdivdiv  11843  divmuleq  11847  divadddiv  11857  divcan5rd  11945  dmdcan2d  11948  mvllmuld  11974  rdiv  11977  subhalfhalf  12376  mul2lt0llt0  13017  mul2lt0lgt0  13018  prodge0ld  13021  xmulcom  13186  modvalr  13794  mulp1mod1  13836  modmul12d  13850  modnegd  13851  modmulmodr  13862  expaddz  14031  binom3  14149  expmulnbnd  14160  digit1  14162  bccmpl  14234  bcm1k  14240  bcn2  14244  bcpasc  14246  recval  15248  abs1m  15261  bhmafibid1cn  15391  bhmafibid2cn  15392  reccn2  15522  lo1mul2  15554  isummulc1  15688  fsummulc1  15710  incexclem  15761  incexc  15762  trireciplem  15787  pwdif  15793  geolim  15795  cvgrat  15808  mertens  15811  ntrivcvgmul  15827  fallfacfwd  15961  bpoly4  15984  fsumcube  15985  eftlub  16036  sinadd  16091  cosadd  16092  sin2t  16104  nndivides  16191  dvds2ln  16218  even2n  16271  oddm1even  16272  mod2eq1n2dvds  16276  m1exp1  16305  pwp1fsum  16320  divalgmod  16335  bitsp1  16360  bitsinv1lem  16370  sadadd2lem  16388  smumullem  16421  gcdmultiplez  16464  mulgcdr  16479  rplpwr  16487  lcmgcdlem  16535  divgcdcoprmex  16595  cncongr1  16596  eulerthlem2  16711  prmdiv  16714  prmdivdiv  16716  vfermltlALT  16732  modprmn0modprm0  16737  coprimeprodsq  16738  pythagtriplem6  16751  pythagtriplem7  16752  pceulem  16775  pcadd  16819  prmpwdvds  16834  mul4sqlem  16883  4sqlem17  16891  mulgassr  19009  odmodnn0  19437  odmulg  19453  odmulgeq  19454  odbezout  19455  odadd1  19745  ablfacrp2  19966  pgpfac1lem3  19976  zringlpirlem3  21389  znunit  21488  icopnfhmeo  24857  cphassr  25128  pjthlem1  25353  itgabs  25752  dvmulbr  25857  dvmulbrOLD  25858  dvcmul  25863  dvcmulf  25864  dvmptcmul  25884  cmvth  25911  cmvthOLD  25912  dvlipcn  25915  c1liplem1  25917  lhop1lem  25934  lhop2  25936  dvcvx  25941  dvfsumlem2  25949  dvfsumlem2OLD  25950  ftc1lem4  25962  itgparts  25970  dvply1  26207  elqaalem3  26245  aalioulem4  26259  taylthlem2  26298  taylthlem2OLD  26299  abelthlem6  26362  abelthlem7  26364  tangtx  26430  tanarg  26544  advlogexp  26580  mulcxp  26610  cxpmul  26613  abscxp  26617  dvcxp2  26666  cxpeq  26683  ang180lem1  26735  lawcoslem1  26741  lawcos  26742  heron  26764  dcubic1  26771  mcubic  26773  cubic2  26774  binom4  26776  dquart  26779  quart1lem  26781  quart1  26782  quartlem1  26783  dvatan  26861  leibpi  26868  log2cnv  26870  efrlim  26895  efrlimOLD  26896  cxp2lim  26903  cxploglim  26904  zetacvg  26941  lgamgulmlem2  26956  lgamgulmlem3  26957  wilthlem1  26994  ftalem1  26999  ftalem5  27003  basellem3  27009  basellem5  27011  mpodvdsmulf1o  27120  dvdsmulf1o  27122  sgmppw  27124  logfac2  27144  chpval2  27145  chpchtsum  27146  perfect1  27155  lgsdirprm  27258  lgsdi  27261  lgsdirnn0  27271  lgsdinn0  27272  gausslemma2dlem1a  27292  gausslemma2dlem6  27299  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  lgsquad2  27313  2lgslem3a1  27327  2lgslem3b1  27328  2lgslem3c1  27329  2lgslem3d1  27330  2lgsoddprmlem2  27336  2sqlem3  27347  2sqlem4  27348  2sqmod  27363  chebbnd1lem2  27397  chebbnd1lem3  27398  chtppilimlem2  27401  chto1lb  27405  rplogsumlem1  27411  dchrisumlem2  27417  dchrvmasum2lem  27423  dchrisum0flblem2  27436  dchrisum0lem2a  27444  mulogsumlem  27458  mulog2sumlem2  27462  selberglem1  27472  selberg2lem  27477  selberg3lem1  27484  selberg4  27488  pntrsumo1  27492  selberg34r  27498  pntrlog2bndlem3  27506  pntrlog2bndlem4  27507  pntlemb  27524  pntlemq  27528  pntlemr  27529  pntlemj  27530  pntlemo  27534  pnt2  27540  pnt  27541  padicabvcxp  27559  ostth2lem2  27561  ostth2lem3  27562  ostth2lem4  27563  ttgcontlem1  28848  brbtwn2  28868  colinearalglem1  28869  colinearalg  28873  axpaschlem  28903  axcontlem8  28934  numclwwlk1  30323  numclwwlk7  30353  smcnlem  30659  pjhthlem1  31353  kbmul  31917  kbass2  32079  submuladdd  32696  muldivdid  32697  pythagreim  32702  quad3d  32706  sgnmul  32793  2exple2exp  32803  psgnfzto1st  33060  zringfrac  33501  ccfldextdgrr  33643  fldext2rspun  33653  fldext2chn  33694  constrrtlc1  33698  constrrtcclem  33700  constrrtcc  33701  constrremulcl  33733  constrmulcl  33737  cos9thpiminplylem1  33748  qqhval2lem  33947  qqhghm  33954  qqhrhm  33955  oddpwdc  34321  plymulx0  34514  signsvtp  34550  signsvtn  34551  signsvfpn  34552  signsvfnn  34553  breprexplemc  34599  circlemethhgt  34610  logdivsqrle  34617  hgt750lemf  34620  hgt750lemb  34623  hgt750leme  34625  subfacval2  35159  subfaclim  35160  fwddifnp1  36138  knoppndvlem11  36495  knoppndvlem17  36501  bj-subcom  37281  bj-bary1lem1  37284  itg2addnclem  37650  itg2addnclem2  37651  itgabsnc  37668  ftc1cnnclem  37670  areacirclem1  37687  areacirc  37692  geomcau  37738  bfplem1  37801  rrndstprj2  37810  rrnequiv  37814  lcmineqlem1  42002  lcmineqlem5  42006  lcmineqlem8  42009  lcmineqlem11  42012  lcmineqlem18  42019  lcmineqlem21  42022  3lexlogpow5ineq2  42028  3lexlogpow2ineq1  42031  dvrelogpow2b  42041  aks4d1p1p7  42047  primrootscoprmpow  42072  primrootscoprbij  42075  aks6d1c1  42089  aks6d1c2  42103  2np3bcnp1  42117  2ap1caineq  42118  bcle2d  42152  aks6d1c7lem1  42153  nicomachus  42285  retire  42292  readvrec  42335  3cubeslem2  42658  3cubeslem3l  42659  3cubeslem3r  42660  irrapxlem5  42799  pellexlem2  42803  pellexlem6  42807  qirropth  42881  rmxyadd  42894  rmxm1  42907  rmxluc  42909  rmyluc2  42911  rmydbl  42913  jm2.24nn  42932  jm2.17a  42933  jm2.17b  42934  jm2.17c  42935  jm2.18  42961  jm2.19lem2  42963  jm2.22  42968  jm2.23  42969  areaquad  43189  imo72b2  44145  int-mulcomd  44149  int-rightdistd  44153  cvgdvgrat  44286  radcnvrat  44287  bccm1k  44315  binomcxplemwb  44321  binomcxplemnotnn0  44329  sineq0ALT  44910  mul13d  45262  divdiv3d  45339  mccllem  45579  coskpi2  45848  cosknegpi  45851  dvsinax  45895  dvasinbx  45902  dvcosax  45908  dvnxpaek  45924  dvnmul  45925  dvnprodlem2  45929  itgsinexplem1  45936  stoweidlem1  45983  stoweidlem11  45993  stoweidlem26  46008  stoweidlem32  46014  wallispilem4  46050  wallispi2lem1  46053  wallispi2lem2  46054  stirlinglem3  46058  stirlinglem4  46059  stirlinglem5  46060  stirlinglem7  46062  stirlinglem10  46065  stirlinglem15  46070  dirkertrigeqlem1  46080  dirkertrigeqlem2  46081  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem1  46085  fourierdlem16  46105  fourierdlem21  46110  fourierdlem22  46111  fourierdlem56  46144  fourierdlem66  46154  fourierdlem83  46171  fourierswlem  46212  fouriersw  46213  etransclem23  46239  etransclem24  46240  etransclem38  46254  etransclem46  46262  hoiprodp1  46570  hoidmvlelem2  46578  smfmullem1  46773  sigarac  46834  sigarls  46839  sigarid  46840  sigardiv  46843  sigarcol  46846  sigaradd  46848  cevathlem1  46849  sqrtnegnre  47292  fmtnoodd  47518  sqrtpwpw2p  47523  fmtnorec3  47533  fmtnoprmfac2lem1  47551  fmtnofac1  47555  lighneallem2  47591  lighneallem3  47592  proththd  47599  requad01  47606  dfeven2  47634  fppr2odd  47716  fpprwppr  47724  altgsumbc  48324  altgsumbcALT  48325  blennnt2  48562  dignn0flhalflem2  48589  dignn0ehalf  48590  itcovalt2lem2lem2  48647  affinecomb2  48676  rrx2linest  48715  itscnhlc0yqe  48732  itsclc0yqsollem1  48735  itscnhlc0xyqsol  48738  itschlc0xyqsol1  48739  itsclc0xyqsolr  48742  itsclquadb  48749  2itscplem3  48753  itscnhlinecirc02plem1  48755  itscnhlinecirc02plem2  48756  inlinecirc02p  48760  amgmwlem  49775