Theorem mulcomd 11331

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11199   · cmul 11206

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11265

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mul31  11478  mul4r  11480  mulcand  11950  mulcan2d  11951  divcan1  11984  divrec2  11992  div23  11994  muldivdid  12012  divdivdiv  12019  divmuleq  12023  divadddiv  12033  divcan5rd  12121  dmdcan2d  12124  mvllmuld  12150  rdiv  12153  subhalfhalf  12581  mul2lt0llt0  13227  mul2lt0lgt0  13228  prodge0ld  13231  xmulcom  13397  modvalr  14013  mulp1mod1  14055  modmul12d  14069  modnegd  14070  modmulmodr  14081  expaddz  14250  binom3  14369  expmulnbnd  14380  digit1  14382  bccmpl  14454  bcm1k  14460  bcn2  14464  bcpasc  14466  sgnmul  15261  recval  15491  abs1m  15504  bhmafibid1cn  15634  bhmafibid2cn  15635  reccn2  15765  lo1mul2  15797  isummulc1  15930  fsummulc1  15952  incexclem  16006  incexc  16007  trireciplem  16032  pwdif  16038  geolim  16040  cvgrat  16053  mertens  16056  ntrivcvgmul  16072  fallfacfwd  16203  bpoly4  16226  fsumcube  16227  eftlub  16278  sinadd  16333  cosadd  16334  sin2t  16346  nndivides  16433  dvds2ln  16460  even2n  16513  oddm1even  16514  mod2eq1n2dvds  16518  m1exp1  16547  pwp1fsum  16562  divalgmod  16577  bitsp1  16602  bitsinv1lem  16612  sadadd2lem  16630  smumullem  16663  gcdmultiplez  16709  mulgcdr  16724  rplpwr  16733  lcmgcdlem  16782  divgcdcoprmex  16842  cncongr1  16843  eulerthlem2  16960  prmdiv  16963  prmdivdiv  16965  vfermltlALT  16981  modprmn0modprm0  16986  coprimeprodsq  16987  pythagtriplem6  17000  pythagtriplem7  17001  pceulem  17024  pcadd  17068  prmpwdvds  17083  mul4sqlem  17132  4sqlem17  17140  mulgassr  19323  odmodnn0  19755  odmulg  19771  odmulgeq  19772  odbezout  19773  odadd1  20063  ablfacrp2  20284  pgpfac1lem3  20294  zringlpirlem3  21771  znunit  21870  icopnfhmeo  25265  cphassr  25534  pjthlem1  25759  itgabs  26156  dvmulbr  26260  dvcmul  26265  dvcmulf  26266  dvmptcmul  26285  cmvth  26312  dvlipcn  26315  c1liplem1  26317  lhop1lem  26334  lhop2  26336  dvcvx  26341  dvfsumlem2  26348  ftc1lem4  26360  itgparts  26368  plyn0mulidp  26603  dvply1  26606  elqaalem3  26645  aalioulem4  26663  taylthlem2  26702  abelthlem6  26764  abelthlem7  26766  tangtx  26835  tanarg  26948  advlogexp  26984  mulcxp  27014  cxpmul  27017  abscxp  27021  dvcxp2  27070  cxpeq  27086  ang180lem1  27138  lawcoslem1  27144  lawcos  27145  heron  27167  dcubic1  27174  mcubic  27176  cubic2  27177  binom4  27179  dquart  27182  quart1lem  27184  quart1  27185  quartlem1  27186  dvatan  27264  leibpi  27271  log2cnv  27273  efrlim  27298  cxp2lim  27305  cxploglim  27306  zetacvg  27343  lgamgulmlem2  27358  lgamgulmlem3  27359  wilthlem1  27396  ftalem1  27401  ftalem5  27405  basellem3  27411  basellem5  27413  basellem8  27416  mpodvdsmulf1o  27522  dvdsmulf1o  27524  sgmppw  27525  logfac2  27545  chpval2  27546  chpchtsum  27547  perfect1  27556  lgsdirprm  27659  lgsdi  27662  lgsdirnn0  27672  lgsdinn0  27673  gausslemma2dlem1a  27693  gausslemma2dlem6  27700  lgsquadlem1  27708  lgsquadlem2  27709  lgsquadlem3  27710  lgsquad2  27714  2lgslem3a1  27728  2lgslem3b1  27729  2lgslem3c1  27730  2lgslem3d1  27731  2lgsoddprmlem2  27737  2sqlem3  27748  2sqlem4  27749  2sqmod  27764  chebbnd1lem2  27798  chebbnd1lem3  27799  chtppilimlem2  27802  chto1lb  27806  rplogsumlem1  27812  dchrisumlem2  27818  dchrvmasum2lem  27824  dchrisum0flblem2  27837  dchrisum0lem2a  27845  mulogsumlem  27859  mulog2sumlem2  27863  selberglem1  27873  selberg2lem  27878  selberg3lem1  27885  selberg4  27889  pntrsumo1  27893  selberg34r  27899  pntrlog2bndlem3  27907  pntrlog2bndlem4  27908  pntlemb  27925  pntlemq  27929  pntlemr  27930  pntlemj  27931  pntlemo  27935  pnt2  27941  pnt  27942  padicabvcxp  27960  ostth2lem2  27962  ostth2lem3  27963  ostth2lem4  27964  ttgcontlem1  29463  brbtwn2  29484  colinearalglem1  29485  colinearalg  29489  axpaschlem  29519  axcontlem8  29550  numclwwlk1  30963  numclwwlk7  30993  smcnlem  31300  pjhthlem1  31994  kbmul  32558  kbass2  32720  submuladdd  33375  pythagreim  33380  quad3d  33384  2exple2exp  33468  psgnfzto1st  33709  zringfrac  34129  ccfldextdgrr  34347  fldext2rspun  34357  fldext2chn  34403  constrrtlc1  34407  constrrtcclem  34409  constrrtcc  34410  constrremulcl  34442  constrmulcl  34446  cos9thpiminplylem1  34457  qqhval2lem  34656  qqhghm  34663  qqhrhm  34664  oddpwdc  35029  signsvtp  35255  signsvtn  35256  signsvfpn  35257  signsvfnn  35258  breprexplemc  35304  circlemethhgt  35315  logdivsqrle  35322  hgt750lemf  35325  hgt750lemb  35328  hgt750leme  35330  subfacval2  36021  subfaclim  36022  fwddifnp1  37005  knoppndvlem11  37463  knoppndvlem17  37469  bj-subcom  38305  bj-bary1lem1  38308  itg2addnclem  38665  itg2addnclem2  38666  itgabsnc  38683  ftc1cnnclem  38685  areacirclem1  38702  areacirc  38707  geomcau  38769  bfplem1  38832  rrndstprj2  38841  rrnequiv  38845  lcmineqlem1  43155  lcmineqlem5  43159  lcmineqlem8  43162  lcmineqlem11  43165  lcmineqlem18  43172  lcmineqlem21  43175  3lexlogpow5ineq2  43181  3lexlogpow2ineq1  43184  dvrelogpow2b  43194  aks4d1p1p7  43200  primrootscoprmpow  43225  primrootscoprbij  43228  aks6d1c1  43242  aks6d1c2  43256  2np3bcnp1  43270  2ap1caineq  43271  bcle2d  43305  aks6d1c7lem1  43306  quadfac  43331  nicomachus  43445  retire  43452  readvrec  43489  3cubeslem2  43771  3cubeslem3l  43772  3cubeslem3r  43773  irrapxlem5  43909  pellexlem2  43913  pellexlem6  43917  qirropth  43991  rmxyadd  44004  rmxm1  44017  rmxluc  44019  rmyluc2  44021  rmydbl  44023  jm2.24nn  44042  jm2.17a  44043  jm2.17b  44044  jm2.17c  44045  jm2.18  44071  jm2.19lem2  44073  jm2.22  44078  jm2.23  44079  areaquad  44294  imo72b2  45248  int-mulcomd  45252  int-rightdistd  45256  cvgdvgrat  45373  radcnvrat  45374  bccm1k  45402  binomcxplemwb  45408  binomcxplemnotnn0  45416  sineq0ALT  45995  mul13d  46372  divdiv3d  46447  mccllem  46685  coskpi2  46952  cosknegpi  46955  dvsinax  46999  dvasinbx  47006  dvcosax  47012  dvnxpaek  47028  dvnmul  47029  dvnprodlem2  47033  itgsinexplem1  47040  stoweidlem1  47087  stoweidlem11  47097  stoweidlem26  47112  stoweidlem32  47118  wallispilem4  47154  wallispi2lem1  47157  wallispi2lem2  47158  stirlinglem3  47162  stirlinglem4  47163  stirlinglem5  47164  stirlinglem7  47166  stirlinglem10  47169  stirlinglem15  47174  dirkertrigeqlem1  47184  dirkertrigeqlem2  47185  dirkertrigeqlem3  47186  dirkertrigeq  47187  dirkercncflem1  47189  fourierdlem16  47209  fourierdlem21  47214  fourierdlem22  47215  fourierdlem56  47248  fourierdlem66  47258  fourierdlem83  47275  fourierswlem  47316  fouriersw  47317  etransclem23  47343  etransclem24  47344  etransclem38  47358  etransclem46  47366  hoiprodp1  47674  hoidmvlelem2  47682  smfmullem1  47877  sigarac  47938  sigarls  47943  sigarid  47944  sigardiv  47947  sigarcol  47950  sigaradd  47952  cevathlem1  47953  sin3t  47993  cos3t  47994  sin5tlem1  47995  sin5tlem3  47997  sqrtnegnre  48453  fmtnoodd  48694  sqrtpwpw2p  48699  fmtnorec3  48709  fmtnoprmfac2lem1  48727  fmtnofac1  48731  lighneallem2  48767  lighneallem3  48768  proththd  48775  requad01  48795  dfeven2  48823  fppr2odd  48905  fpprwppr  48913  altgsumbc  49540  altgsumbcALT  49541  blennnt2  49777  dignn0flhalflem2  49804  dignn0ehalf  49805  itcovalt2lem2lem2  49862  affinecomb2  49891  rrx2linest  49930  itscnhlc0yqe  49947  itsclc0yqsollem1  49950  itscnhlc0xyqsol  49953  itschlc0xyqsol1  49954  itsclc0xyqsolr  49957  itsclquadb  49964  2itscplem3  49968  itscnhlinecirc02plem1  49970  itscnhlinecirc02plem2  49971  inlinecirc02p  49975  crosspaltd  51042  crossp3d  51043  amgmwlem  51063