Theorem mulcomd 11202

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   · cmul 11080

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

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

This theorem is referenced by:  mul31  11348  mul4r  11350  mulcand  11818  mulcan2d  11819  divcan1  11853  divrec2  11861  div23  11863  divdivdiv  11890  divmuleq  11894  divadddiv  11904  divcan5rd  11992  dmdcan2d  11995  mvllmuld  12021  rdiv  12024  subhalfhalf  12423  mul2lt0llt0  13064  mul2lt0lgt0  13065  prodge0ld  13068  xmulcom  13233  modvalr  13841  mulp1mod1  13883  modmul12d  13897  modnegd  13898  modmulmodr  13909  expaddz  14078  binom3  14196  expmulnbnd  14207  digit1  14209  bccmpl  14281  bcm1k  14287  bcn2  14291  bcpasc  14293  recval  15296  abs1m  15309  bhmafibid1cn  15439  bhmafibid2cn  15440  reccn2  15570  lo1mul2  15602  isummulc1  15736  fsummulc1  15758  incexclem  15809  incexc  15810  trireciplem  15835  pwdif  15841  geolim  15843  cvgrat  15856  mertens  15859  ntrivcvgmul  15875  fallfacfwd  16009  bpoly4  16032  fsumcube  16033  eftlub  16084  sinadd  16139  cosadd  16140  sin2t  16152  nndivides  16239  dvds2ln  16266  even2n  16319  oddm1even  16320  mod2eq1n2dvds  16324  m1exp1  16353  pwp1fsum  16368  divalgmod  16383  bitsp1  16408  bitsinv1lem  16418  sadadd2lem  16436  smumullem  16469  gcdmultiplez  16512  mulgcdr  16527  rplpwr  16535  lcmgcdlem  16583  divgcdcoprmex  16643  cncongr1  16644  eulerthlem2  16759  prmdiv  16762  prmdivdiv  16764  vfermltlALT  16780  modprmn0modprm0  16785  coprimeprodsq  16786  pythagtriplem6  16799  pythagtriplem7  16800  pceulem  16823  pcadd  16867  prmpwdvds  16882  mul4sqlem  16931  4sqlem17  16939  mulgassr  19051  odmodnn0  19477  odmulg  19493  odmulgeq  19494  odbezout  19495  odadd1  19785  ablfacrp2  20006  pgpfac1lem3  20016  zringlpirlem3  21381  znunit  21480  icopnfhmeo  24848  cphassr  25119  pjthlem1  25344  itgabs  25743  dvmulbr  25848  dvmulbrOLD  25849  dvcmul  25854  dvcmulf  25855  dvmptcmul  25875  cmvth  25902  cmvthOLD  25903  dvlipcn  25906  c1liplem1  25908  lhop1lem  25925  lhop2  25927  dvcvx  25932  dvfsumlem2  25940  dvfsumlem2OLD  25941  ftc1lem4  25953  itgparts  25961  dvply1  26198  elqaalem3  26236  aalioulem4  26250  taylthlem2  26289  taylthlem2OLD  26290  abelthlem6  26353  abelthlem7  26355  tangtx  26421  tanarg  26535  advlogexp  26571  mulcxp  26601  cxpmul  26604  abscxp  26608  dvcxp2  26657  cxpeq  26674  ang180lem1  26726  lawcoslem1  26732  lawcos  26733  heron  26755  dcubic1  26762  mcubic  26764  cubic2  26765  binom4  26767  dquart  26770  quart1lem  26772  quart1  26773  quartlem1  26774  dvatan  26852  leibpi  26859  log2cnv  26861  efrlim  26886  efrlimOLD  26887  cxp2lim  26894  cxploglim  26895  zetacvg  26932  lgamgulmlem2  26947  lgamgulmlem3  26948  wilthlem1  26985  ftalem1  26990  ftalem5  26994  basellem3  27000  basellem5  27002  mpodvdsmulf1o  27111  dvdsmulf1o  27113  sgmppw  27115  logfac2  27135  chpval2  27136  chpchtsum  27137  perfect1  27146  lgsdirprm  27249  lgsdi  27252  lgsdirnn0  27262  lgsdinn0  27263  gausslemma2dlem1a  27283  gausslemma2dlem6  27290  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  lgsquad2  27304  2lgslem3a1  27318  2lgslem3b1  27319  2lgslem3c1  27320  2lgslem3d1  27321  2lgsoddprmlem2  27327  2sqlem3  27338  2sqlem4  27339  2sqmod  27354  chebbnd1lem2  27388  chebbnd1lem3  27389  chtppilimlem2  27392  chto1lb  27396  rplogsumlem1  27402  dchrisumlem2  27408  dchrvmasum2lem  27414  dchrisum0flblem2  27427  dchrisum0lem2a  27435  mulogsumlem  27449  mulog2sumlem2  27453  selberglem1  27463  selberg2lem  27468  selberg3lem1  27475  selberg4  27479  pntrsumo1  27483  selberg34r  27489  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntlemb  27515  pntlemq  27519  pntlemr  27520  pntlemj  27521  pntlemo  27525  pnt2  27531  pnt  27532  padicabvcxp  27550  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ttgcontlem1  28819  brbtwn2  28839  colinearalglem1  28840  colinearalg  28844  axpaschlem  28874  axcontlem8  28905  numclwwlk1  30297  numclwwlk7  30327  smcnlem  30633  pjhthlem1  31327  kbmul  31891  kbass2  32053  submuladdd  32670  muldivdid  32671  pythagreim  32676  quad3d  32680  sgnmul  32767  2exple2exp  32777  psgnfzto1st  33069  zringfrac  33532  ccfldextdgrr  33674  fldext2rspun  33684  fldext2chn  33725  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  constrremulcl  33764  constrmulcl  33768  cos9thpiminplylem1  33779  qqhval2lem  33978  qqhghm  33985  qqhrhm  33986  oddpwdc  34352  plymulx0  34545  signsvtp  34581  signsvtn  34582  signsvfpn  34583  signsvfnn  34584  breprexplemc  34630  circlemethhgt  34641  logdivsqrle  34648  hgt750lemf  34651  hgt750lemb  34654  hgt750leme  34656  subfacval2  35181  subfaclim  35182  fwddifnp1  36160  knoppndvlem11  36517  knoppndvlem17  36523  bj-subcom  37303  bj-bary1lem1  37306  itg2addnclem  37672  itg2addnclem2  37673  itgabsnc  37690  ftc1cnnclem  37692  areacirclem1  37709  areacirc  37714  geomcau  37760  bfplem1  37823  rrndstprj2  37832  rrnequiv  37836  lcmineqlem1  42024  lcmineqlem5  42028  lcmineqlem8  42031  lcmineqlem11  42034  lcmineqlem18  42041  lcmineqlem21  42044  3lexlogpow5ineq2  42050  3lexlogpow2ineq1  42053  dvrelogpow2b  42063  aks4d1p1p7  42069  primrootscoprmpow  42094  primrootscoprbij  42097  aks6d1c1  42111  aks6d1c2  42125  2np3bcnp1  42139  2ap1caineq  42140  bcle2d  42174  aks6d1c7lem1  42175  nicomachus  42307  retire  42314  readvrec  42357  3cubeslem2  42680  3cubeslem3l  42681  3cubeslem3r  42682  irrapxlem5  42821  pellexlem2  42825  pellexlem6  42829  qirropth  42903  rmxyadd  42917  rmxm1  42930  rmxluc  42932  rmyluc2  42934  rmydbl  42936  jm2.24nn  42955  jm2.17a  42956  jm2.17b  42957  jm2.17c  42958  jm2.18  42984  jm2.19lem2  42986  jm2.22  42991  jm2.23  42992  areaquad  43212  imo72b2  44168  int-mulcomd  44172  int-rightdistd  44176  cvgdvgrat  44309  radcnvrat  44310  bccm1k  44338  binomcxplemwb  44344  binomcxplemnotnn0  44352  sineq0ALT  44933  mul13d  45285  divdiv3d  45362  mccllem  45602  coskpi2  45871  cosknegpi  45874  dvsinax  45918  dvasinbx  45925  dvcosax  45931  dvnxpaek  45947  dvnmul  45948  dvnprodlem2  45952  itgsinexplem1  45959  stoweidlem1  46006  stoweidlem11  46016  stoweidlem26  46031  stoweidlem32  46037  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem7  46085  stirlinglem10  46088  stirlinglem15  46093  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem1  46108  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem56  46167  fourierdlem66  46177  fourierdlem83  46194  fourierswlem  46235  fouriersw  46236  etransclem23  46262  etransclem24  46263  etransclem38  46277  etransclem46  46285  hoiprodp1  46593  hoidmvlelem2  46601  smfmullem1  46796  sigarac  46857  sigarls  46862  sigarid  46863  sigardiv  46866  sigarcol  46869  sigaradd  46871  cevathlem1  46872  sqrtnegnre  47312  fmtnoodd  47538  sqrtpwpw2p  47543  fmtnorec3  47553  fmtnoprmfac2lem1  47571  fmtnofac1  47575  lighneallem2  47611  lighneallem3  47612  proththd  47619  requad01  47626  dfeven2  47654  fppr2odd  47736  fpprwppr  47744  altgsumbc  48344  altgsumbcALT  48345  blennnt2  48582  dignn0flhalflem2  48609  dignn0ehalf  48610  itcovalt2lem2lem2  48667  affinecomb2  48696  rrx2linest  48735  itscnhlc0yqe  48752  itsclc0yqsollem1  48755  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itsclc0xyqsolr  48762  itsclquadb  48769  2itscplem3  48773  itscnhlinecirc02plem1  48775  itscnhlinecirc02plem2  48776  inlinecirc02p  48780  amgmwlem  49795