Theorem mulcomd 11166

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   · cmul 11043

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

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

This theorem is referenced by:  mul31  11313  mul4r  11315  mulcand  11783  mulcan2d  11784  divcan1  11818  divrec2  11826  div23  11828  muldivdid  11849  divdivdiv  11856  divmuleq  11860  divadddiv  11870  divcan5rd  11958  dmdcan2d  11961  mvllmuld  11987  rdiv  11990  subhalfhalf  12411  mul2lt0llt0  13048  mul2lt0lgt0  13049  prodge0ld  13052  xmulcom  13218  modvalr  13831  mulp1mod1  13873  modmul12d  13887  modnegd  13888  modmulmodr  13899  expaddz  14068  binom3  14186  expmulnbnd  14197  digit1  14199  bccmpl  14271  bcm1k  14277  bcn2  14281  bcpasc  14283  recval  15285  abs1m  15298  bhmafibid1cn  15428  bhmafibid2cn  15429  reccn2  15559  lo1mul2  15591  isummulc1  15725  fsummulc1  15747  incexclem  15801  incexc  15802  trireciplem  15827  pwdif  15833  geolim  15835  cvgrat  15848  mertens  15851  ntrivcvgmul  15867  fallfacfwd  16001  bpoly4  16024  fsumcube  16025  eftlub  16076  sinadd  16131  cosadd  16132  sin2t  16144  nndivides  16231  dvds2ln  16258  even2n  16311  oddm1even  16312  mod2eq1n2dvds  16316  m1exp1  16345  pwp1fsum  16360  divalgmod  16375  bitsp1  16400  bitsinv1lem  16410  sadadd2lem  16428  smumullem  16461  gcdmultiplez  16504  mulgcdr  16519  rplpwr  16527  lcmgcdlem  16575  divgcdcoprmex  16635  cncongr1  16636  eulerthlem2  16752  prmdiv  16755  prmdivdiv  16757  vfermltlALT  16773  modprmn0modprm0  16778  coprimeprodsq  16779  pythagtriplem6  16792  pythagtriplem7  16793  pceulem  16816  pcadd  16860  prmpwdvds  16875  mul4sqlem  16924  4sqlem17  16932  mulgassr  19088  odmodnn0  19515  odmulg  19531  odmulgeq  19532  odbezout  19533  odadd1  19823  ablfacrp2  20044  pgpfac1lem3  20054  zringlpirlem3  21444  znunit  21543  icopnfhmeo  24910  cphassr  25179  pjthlem1  25404  itgabs  25802  dvmulbr  25906  dvcmul  25911  dvcmulf  25912  dvmptcmul  25931  cmvth  25958  dvlipcn  25961  c1liplem1  25963  lhop1lem  25980  lhop2  25982  dvcvx  25987  dvfsumlem2  25994  ftc1lem4  26006  itgparts  26014  dvply1  26250  elqaalem3  26287  aalioulem4  26301  taylthlem2  26339  abelthlem6  26401  abelthlem7  26403  tangtx  26469  tanarg  26583  advlogexp  26619  mulcxp  26649  cxpmul  26652  abscxp  26656  dvcxp2  26705  cxpeq  26721  ang180lem1  26773  lawcoslem1  26779  lawcos  26780  heron  26802  dcubic1  26809  mcubic  26811  cubic2  26812  binom4  26814  dquart  26817  quart1lem  26819  quart1  26820  quartlem1  26821  dvatan  26899  leibpi  26906  log2cnv  26908  efrlim  26933  cxp2lim  26940  cxploglim  26941  zetacvg  26978  lgamgulmlem2  26993  lgamgulmlem3  26994  wilthlem1  27031  ftalem1  27036  ftalem5  27040  basellem3  27046  basellem5  27048  mpodvdsmulf1o  27157  dvdsmulf1o  27159  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  28953  brbtwn2  28974  colinearalglem1  28975  colinearalg  28979  axpaschlem  29009  axcontlem8  29040  numclwwlk1  30431  numclwwlk7  30461  smcnlem  30768  pjhthlem1  31462  kbmul  32026  kbass2  32188  submuladdd  32813  pythagreim  32818  quad3d  32822  sgnmul  32908  2exple2exp  32918  psgnfzto1st  33166  zringfrac  33614  ccfldextdgrr  33816  fldext2rspun  33826  fldext2chn  33872  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  constrremulcl  33911  constrmulcl  33915  cos9thpiminplylem1  33926  qqhval2lem  34125  qqhghm  34132  qqhrhm  34133  oddpwdc  34498  plymulx0  34691  signsvtp  34727  signsvtn  34728  signsvfpn  34729  signsvfnn  34730  breprexplemc  34776  circlemethhgt  34787  logdivsqrle  34794  hgt750lemf  34797  hgt750lemb  34800  hgt750leme  34802  subfacval2  35369  subfaclim  35370  fwddifnp1  36347  knoppndvlem11  36782  knoppndvlem17  36788  bj-subcom  37622  bj-bary1lem1  37625  itg2addnclem  37992  itg2addnclem2  37993  itgabsnc  38010  ftc1cnnclem  38012  areacirclem1  38029  areacirc  38034  geomcau  38080  bfplem1  38143  rrndstprj2  38152  rrnequiv  38156  lcmineqlem1  42468  lcmineqlem5  42472  lcmineqlem8  42475  lcmineqlem11  42478  lcmineqlem18  42485  lcmineqlem21  42488  3lexlogpow5ineq2  42494  3lexlogpow2ineq1  42497  dvrelogpow2b  42507  aks4d1p1p7  42513  primrootscoprmpow  42538  primrootscoprbij  42541  aks6d1c1  42555  aks6d1c2  42569  2np3bcnp1  42583  2ap1caineq  42584  bcle2d  42618  aks6d1c7lem1  42619  nicomachus  42744  retire  42751  readvrec  42794  3cubeslem2  43117  3cubeslem3l  43118  3cubeslem3r  43119  irrapxlem5  43254  pellexlem2  43258  pellexlem6  43262  qirropth  43336  rmxyadd  43349  rmxm1  43362  rmxluc  43364  rmyluc2  43366  rmydbl  43368  jm2.24nn  43387  jm2.17a  43388  jm2.17b  43389  jm2.17c  43390  jm2.18  43416  jm2.19lem2  43418  jm2.22  43423  jm2.23  43424  areaquad  43644  imo72b2  44599  int-mulcomd  44603  int-rightdistd  44607  cvgdvgrat  44740  radcnvrat  44741  bccm1k  44769  binomcxplemwb  44775  binomcxplemnotnn0  44783  sineq0ALT  45363  mul13d  45713  divdiv3d  45789  mccllem  46027  coskpi2  46294  cosknegpi  46297  dvsinax  46341  dvasinbx  46348  dvcosax  46354  dvnxpaek  46370  dvnmul  46371  dvnprodlem2  46375  itgsinexplem1  46382  stoweidlem1  46429  stoweidlem11  46439  stoweidlem26  46454  stoweidlem32  46460  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem7  46508  stirlinglem10  46511  stirlinglem15  46516  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem1  46531  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem56  46590  fourierdlem66  46600  fourierdlem83  46617  fourierswlem  46658  fouriersw  46659  etransclem23  46685  etransclem24  46686  etransclem38  46700  etransclem46  46708  hoiprodp1  47016  hoidmvlelem2  47024  smfmullem1  47219  sigarac  47280  sigarls  47285  sigarid  47286  sigardiv  47289  sigarcol  47292  sigaradd  47294  cevathlem1  47295  sin3t  47317  cos3t  47318  sin5tlem1  47319  sin5tlem3  47321  sqrtnegnre  47749  fmtnoodd  47990  sqrtpwpw2p  47995  fmtnorec3  48005  fmtnoprmfac2lem1  48023  fmtnofac1  48027  lighneallem2  48063  lighneallem3  48064  proththd  48071  requad01  48091  dfeven2  48119  fppr2odd  48201  fpprwppr  48209  altgsumbc  48822  altgsumbcALT  48823  blennnt2  49059  dignn0flhalflem2  49086  dignn0ehalf  49087  itcovalt2lem2lem2  49144  affinecomb2  49173  rrx2linest  49212  itscnhlc0yqe  49229  itsclc0yqsollem1  49232  itscnhlc0xyqsol  49235  itschlc0xyqsol1  49236  itsclc0xyqsolr  49239  itsclquadb  49246  2itscplem3  49250  itscnhlinecirc02plem1  49252  itscnhlinecirc02plem2  49253  inlinecirc02p  49257  amgmwlem  50271