Theorem mulcomd 11218

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mul31  11365  mul4r  11367  mulcand  11835  mulcan2d  11836  divcan1  11869  divrec2  11877  div23  11879  muldivdid  11900  divdivdiv  11907  divmuleq  11911  divadddiv  11921  divcan5rd  12009  dmdcan2d  12012  mvllmuld  12038  rdiv  12041  subhalfhalf  12469  mul2lt0llt0  13113  mul2lt0lgt0  13114  prodge0ld  13117  xmulcom  13283  modvalr  13896  mulp1mod1  13938  modmul12d  13952  modnegd  13953  modmulmodr  13964  expaddz  14133  binom3  14251  expmulnbnd  14262  digit1  14264  bccmpl  14336  bcm1k  14342  bcn2  14346  bcpasc  14348  sgnmul  15134  recval  15364  abs1m  15377  bhmafibid1cn  15507  bhmafibid2cn  15508  reccn2  15638  lo1mul2  15670  isummulc1  15804  fsummulc1  15826  incexclem  15880  incexc  15881  trireciplem  15906  pwdif  15912  geolim  15914  cvgrat  15927  mertens  15930  ntrivcvgmul  15946  fallfacfwd  16080  bpoly4  16103  fsumcube  16104  eftlub  16155  sinadd  16210  cosadd  16211  sin2t  16223  nndivides  16310  dvds2ln  16337  even2n  16390  oddm1even  16391  mod2eq1n2dvds  16395  m1exp1  16424  pwp1fsum  16439  divalgmod  16454  bitsp1  16479  bitsinv1lem  16489  sadadd2lem  16507  smumullem  16540  gcdmultiplez  16583  mulgcdr  16598  rplpwr  16606  lcmgcdlem  16654  divgcdcoprmex  16714  cncongr1  16715  eulerthlem2  16831  prmdiv  16834  prmdivdiv  16836  vfermltlALT  16852  modprmn0modprm0  16857  coprimeprodsq  16858  pythagtriplem6  16871  pythagtriplem7  16872  pceulem  16895  pcadd  16939  prmpwdvds  16954  mul4sqlem  17003  4sqlem17  17011  mulgassr  19169  odmodnn0  19601  odmulg  19617  odmulgeq  19618  odbezout  19619  odadd1  19909  ablfacrp2  20130  pgpfac1lem3  20140  zringlpirlem3  21574  znunit  21673  icopnfhmeo  25063  cphassr  25332  pjthlem1  25557  itgabs  25955  dvmulbr  26059  dvcmul  26064  dvcmulf  26065  dvmptcmul  26084  cmvth  26111  dvlipcn  26114  c1liplem1  26116  lhop1lem  26133  lhop2  26135  dvcvx  26140  dvfsumlem2  26147  ftc1lem4  26159  itgparts  26167  plyn0mulidp  26403  dvply1  26406  elqaalem3  26443  aalioulem4  26457  taylthlem2  26495  abelthlem6  26557  abelthlem7  26559  tangtx  26628  tanarg  26742  advlogexp  26778  mulcxp  26808  cxpmul  26811  abscxp  26815  dvcxp2  26864  cxpeq  26880  ang180lem1  26932  lawcoslem1  26938  lawcos  26939  heron  26961  dcubic1  26968  mcubic  26970  cubic2  26971  binom4  26973  dquart  26976  quart1lem  26978  quart1  26979  quartlem1  26980  dvatan  27058  leibpi  27065  log2cnv  27067  efrlim  27092  cxp2lim  27099  cxploglim  27100  zetacvg  27137  lgamgulmlem2  27152  lgamgulmlem3  27153  wilthlem1  27190  ftalem1  27195  ftalem5  27199  basellem3  27205  basellem5  27207  mpodvdsmulf1o  27316  dvdsmulf1o  27318  sgmppw  27319  logfac2  27339  chpval2  27340  chpchtsum  27341  perfect1  27350  lgsdirprm  27453  lgsdi  27456  lgsdirnn0  27466  lgsdinn0  27467  gausslemma2dlem1a  27487  gausslemma2dlem6  27494  lgsquadlem1  27502  lgsquadlem2  27503  lgsquadlem3  27504  lgsquad2  27508  2lgslem3a1  27522  2lgslem3b1  27523  2lgslem3c1  27524  2lgslem3d1  27525  2lgsoddprmlem2  27531  2sqlem3  27542  2sqlem4  27543  2sqmod  27558  chebbnd1lem2  27592  chebbnd1lem3  27593  chtppilimlem2  27596  chto1lb  27600  rplogsumlem1  27606  dchrisumlem2  27612  dchrvmasum2lem  27618  dchrisum0flblem2  27631  dchrisum0lem2a  27639  mulogsumlem  27653  mulog2sumlem2  27657  selberglem1  27667  selberg2lem  27672  selberg3lem1  27679  selberg4  27683  pntrsumo1  27687  selberg34r  27693  pntrlog2bndlem3  27701  pntrlog2bndlem4  27702  pntlemb  27719  pntlemq  27723  pntlemr  27724  pntlemj  27725  pntlemo  27729  pnt2  27735  pnt  27736  padicabvcxp  27754  ostth2lem2  27756  ostth2lem3  27757  ostth2lem4  27758  ttgcontlem1  29143  brbtwn2  29164  colinearalglem1  29165  colinearalg  29169  axpaschlem  29199  axcontlem8  29230  numclwwlk1  30621  numclwwlk7  30651  smcnlem  30958  pjhthlem1  31652  kbmul  32216  kbass2  32378  submuladdd  32997  pythagreim  33002  quad3d  33006  2exple2exp  33091  psgnfzto1st  33338  zringfrac  33761  ccfldextdgrr  33979  fldext2rspun  33989  fldext2chn  34035  constrrtlc1  34039  constrrtcclem  34041  constrrtcc  34042  constrremulcl  34074  constrmulcl  34078  cos9thpiminplylem1  34089  qqhval2lem  34288  qqhghm  34295  qqhrhm  34296  oddpwdc  34661  signsvtp  34887  signsvtn  34888  signsvfpn  34889  signsvfnn  34890  breprexplemc  34936  circlemethhgt  34947  logdivsqrle  34954  hgt750lemf  34957  hgt750lemb  34960  hgt750leme  34962  subfacval2  35550  subfaclim  35551  fwddifnp1  36528  knoppndvlem11  36973  knoppndvlem17  36979  bj-subcom  37812  bj-bary1lem1  37815  itg2addnclem  38182  itg2addnclem2  38183  itgabsnc  38200  ftc1cnnclem  38202  areacirclem1  38219  areacirc  38224  geomcau  38270  bfplem1  38333  rrndstprj2  38342  rrnequiv  38346  lcmineqlem1  42658  lcmineqlem5  42662  lcmineqlem8  42665  lcmineqlem11  42668  lcmineqlem18  42675  lcmineqlem21  42678  3lexlogpow5ineq2  42684  3lexlogpow2ineq1  42687  dvrelogpow2b  42697  aks4d1p1p7  42703  primrootscoprmpow  42728  primrootscoprbij  42731  aks6d1c1  42745  aks6d1c2  42759  2np3bcnp1  42773  2ap1caineq  42774  bcle2d  42808  aks6d1c7lem1  42809  nicomachus  42933  retire  42940  readvrec  42983  3cubeslem2  43278  3cubeslem3l  43279  3cubeslem3r  43280  irrapxlem5  43415  pellexlem2  43419  pellexlem6  43423  qirropth  43497  rmxyadd  43510  rmxm1  43523  rmxluc  43525  rmyluc2  43527  rmydbl  43529  jm2.24nn  43548  jm2.17a  43549  jm2.17b  43550  jm2.17c  43551  jm2.18  43577  jm2.19lem2  43579  jm2.22  43584  jm2.23  43585  areaquad  43805  imo72b2  44760  int-mulcomd  44764  int-rightdistd  44768  cvgdvgrat  44887  radcnvrat  44888  bccm1k  44916  binomcxplemwb  44922  binomcxplemnotnn0  44930  sineq0ALT  45510  mul13d  45857  divdiv3d  45933  mccllem  46171  coskpi2  46438  cosknegpi  46441  dvsinax  46485  dvasinbx  46492  dvcosax  46498  dvnxpaek  46514  dvnmul  46515  dvnprodlem2  46519  itgsinexplem1  46526  stoweidlem1  46573  stoweidlem11  46583  stoweidlem26  46598  stoweidlem32  46604  wallispilem4  46640  wallispi2lem1  46643  wallispi2lem2  46644  stirlinglem3  46648  stirlinglem4  46649  stirlinglem5  46650  stirlinglem7  46652  stirlinglem10  46655  stirlinglem15  46660  dirkertrigeqlem1  46670  dirkertrigeqlem2  46671  dirkertrigeqlem3  46672  dirkertrigeq  46673  dirkercncflem1  46675  fourierdlem16  46695  fourierdlem21  46700  fourierdlem22  46701  fourierdlem56  46734  fourierdlem66  46744  fourierdlem83  46761  fourierswlem  46802  fouriersw  46803  etransclem23  46829  etransclem24  46830  etransclem38  46844  etransclem46  46852  hoiprodp1  47160  hoidmvlelem2  47168  smfmullem1  47363  sigarac  47424  sigarls  47429  sigarid  47430  sigardiv  47433  sigarcol  47436  sigaradd  47438  cevathlem1  47439  sin3t  47463  cos3t  47464  sin5tlem1  47465  sin5tlem3  47467  sqrtnegnre  47899  fmtnoodd  48140  sqrtpwpw2p  48145  fmtnorec3  48155  fmtnoprmfac2lem1  48173  fmtnofac1  48177  lighneallem2  48213  lighneallem3  48214  proththd  48221  requad01  48241  dfeven2  48269  fppr2odd  48351  fpprwppr  48359  altgsumbc  48983  altgsumbcALT  48984  blennnt2  49220  dignn0flhalflem2  49247  dignn0ehalf  49248  itcovalt2lem2lem2  49305  affinecomb2  49334  rrx2linest  49373  itscnhlc0yqe  49390  itsclc0yqsollem1  49393  itscnhlc0xyqsol  49396  itschlc0xyqsol1  49397  itsclc0xyqsolr  49400  itsclquadb  49407  2itscplem3  49411  itscnhlinecirc02plem1  49413  itscnhlinecirc02plem2  49414  inlinecirc02p  49418  amgmwlem  50431