Theorem mulcomd 11357

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   · cmul 11232

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

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

This theorem is used by:  mul31  11504  mul4r  11506  mulcand  11976  mulcan2d  11977  divcan1  12010  divrec2  12018  div23  12020  muldivdid  12038  divdivdiv  12045  divmuleq  12049  divadddiv  12059  divcan5rd  12147  dmdcan2d  12150  mvllmuld  12176  rdiv  12179  subhalfhalf  12607  mul2lt0llt0  13253  mul2lt0lgt0  13254  prodge0ld  13257  xmulcom  13423  modvalr  14039  mulp1mod1  14081  modmul12d  14095  modnegd  14096  modmulmodr  14107  expaddz  14276  binom3  14395  expmulnbnd  14406  digit1  14408  bccmpl  14480  bcm1k  14486  bcn2  14490  bcpasc  14492  sgnmul  15289  recval  15519  abs1m  15532  bhmafibid1cn  15662  bhmafibid2cn  15663  reccn2  15793  lo1mul2  15825  isummulc1  15958  fsummulc1  15980  incexclem  16034  incexc  16035  trireciplem  16060  pwdif  16066  geolim  16068  cvgrat  16081  mertens  16084  ntrivcvgmul  16100  fallfacfwd  16231  bpoly4  16254  fsumcube  16255  eftlub  16306  sinadd  16361  cosadd  16362  sin2t  16374  nndivides  16461  dvds2ln  16488  even2n  16541  oddm1even  16542  mod2eq1n2dvds  16546  m1exp1  16575  pwp1fsum  16590  divalgmod  16605  bitsp1  16630  bitsinv1lem  16640  sadadd2lem  16658  smumullem  16691  gcdmultiplez  16737  mulgcdr  16752  rplpwr  16761  lcmgcdlem  16810  divgcdcoprmex  16870  cncongr1  16871  eulerthlem2  16988  prmdiv  16991  prmdivdiv  16993  vfermltlALT  17009  modprmn0modprm0  17014  coprimeprodsq  17015  pythagtriplem6  17028  pythagtriplem7  17029  pceulem  17052  pcadd  17096  prmpwdvds  17111  mul4sqlem  17160  4sqlem17  17168  mulgassr  19351  odmodnn0  19784  odmulg  19800  odmulgeq  19801  odbezout  19802  odadd1  20092  ablfacrp2  20313  pgpfac1lem3  20323  zringlpirlem3  21800  znunit  21899  icopnfhmeo  25294  cphassr  25563  pjthlem1  25788  itgabs  26185  dvmulbr  26289  dvcmul  26294  dvcmulf  26295  dvmptcmul  26314  cmvth  26341  dvlipcn  26344  c1liplem1  26346  lhop1lem  26363  lhop2  26365  dvcvx  26370  dvfsumlem2  26377  ftc1lem4  26389  itgparts  26397  plyn0mulidp  26632  dvply1  26635  elqaalem3  26674  aalioulem4  26692  taylthlem2  26731  abelthlem6  26793  abelthlem7  26795  tangtx  26864  tanarg  26977  advlogexp  27013  mulcxp  27043  cxpmul  27046  abscxp  27050  dvcxp2  27099  cxpeq  27115  ang180lem1  27167  lawcoslem1  27173  lawcos  27174  heron  27196  dcubic1  27203  mcubic  27205  cubic2  27206  binom4  27208  dquart  27211  quart1lem  27213  quart1  27214  quartlem1  27215  dvatan  27293  leibpi  27300  log2cnv  27302  efrlim  27327  cxp2lim  27334  cxploglim  27335  zetacvg  27372  lgamgulmlem2  27387  lgamgulmlem3  27388  wilthlem1  27425  ftalem1  27430  ftalem5  27434  basellem3  27440  basellem5  27442  basellem8  27445  mpodvdsmulf1o  27551  dvdsmulf1o  27553  sgmppw  27554  logfac2  27574  chpval2  27575  chpchtsum  27576  perfect1  27585  lgsdirprm  27688  lgsdi  27691  lgsdirnn0  27701  lgsdinn0  27702  gausslemma2dlem1a  27722  gausslemma2dlem6  27729  lgsquadlem1  27737  lgsquadlem2  27738  lgsquadlem3  27739  lgsquad2  27743  2lgslem3a1  27757  2lgslem3b1  27758  2lgslem3c1  27759  2lgslem3d1  27760  2lgsoddprmlem2  27766  2sqlem3  27777  2sqlem4  27778  2sqmod  27793  chebbnd1lem2  27827  chebbnd1lem3  27828  chtppilimlem2  27831  chto1lb  27835  rplogsumlem1  27841  dchrisumlem2  27847  dchrvmasum2lem  27853  dchrisum0flblem2  27866  dchrisum0lem2a  27874  mulogsumlem  27888  mulog2sumlem2  27892  selberglem1  27902  selberg2lem  27907  selberg3lem1  27914  selberg4  27918  pntrsumo1  27922  selberg34r  27928  pntrlog2bndlem3  27936  pntrlog2bndlem4  27937  pntlemb  27954  pntlemq  27958  pntlemr  27959  pntlemj  27960  pntlemo  27964  pnt2  27970  pnt  27971  padicabvcxp  27989  ostth2lem2  27991  ostth2lem3  27992  ostth2lem4  27993  ttgcontlem1  29492  brbtwn2  29513  colinearalglem1  29514  colinearalg  29518  axpaschlem  29548  axcontlem8  29579  numclwwlk1  30992  numclwwlk7  31022  smcnlem  31329  pjhthlem1  32023  kbmul  32587  kbass2  32749  submuladdd  33402  pythagreim  33407  quad3d  33411  2exple2exp  33495  psgnfzto1st  33736  zringfrac  34156  ccfldextdgrr  34374  fldext2rspun  34384  fldext2chn  34430  constrrtlc1  34434  constrrtcclem  34436  constrrtcc  34437  constrremulcl  34469  constrmulcl  34473  cos9thpiminplylem1  34484  qqhval2lem  34683  qqhghm  34690  qqhrhm  34691  oddpwdc  35056  signsvtp  35282  signsvtn  35283  signsvfpn  35284  signsvfnn  35285  breprexplemc  35331  circlemethhgt  35342  logdivsqrle  35349  hgt750lemf  35352  hgt750lemb  35355  hgt750leme  35357  subfacval2  36119  subfaclim  36120  fwddifnp1  37108  knoppndvlem11  37566  knoppndvlem17  37572  bj-subcom  38421  bj-bary1lem1  38424  itg2addnclem  38781  itg2addnclem2  38782  itgabsnc  38799  ftc1cnnclem  38801  areacirclem1  38818  areacirc  38823  geomcau  38885  bfplem1  38948  rrndstprj2  38957  rrnequiv  38961  lcmineqlem1  43271  lcmineqlem5  43275  lcmineqlem8  43278  lcmineqlem11  43281  lcmineqlem18  43288  lcmineqlem21  43291  3lexlogpow5ineq2  43297  3lexlogpow2ineq1  43300  dvrelogpow2b  43310  aks4d1p1p7  43316  primrootscoprmpow  43341  primrootscoprbij  43344  aks6d1c1  43358  aks6d1c2  43372  2np3bcnp1  43386  2ap1caineq  43387  bcle2d  43421  aks6d1c7lem1  43422  quadfac  43447  nicomachus  43562  retire  43569  readvrec  43606  3cubeslem2  43888  3cubeslem3l  43889  3cubeslem3r  43890  irrapxlem5  44026  pellexlem2  44030  pellexlem6  44034  qirropth  44108  rmxyadd  44121  rmxm1  44134  rmxluc  44136  rmyluc2  44138  rmydbl  44140  jm2.24nn  44159  jm2.17a  44160  jm2.17b  44161  jm2.17c  44162  jm2.18  44188  jm2.19lem2  44190  jm2.22  44195  jm2.23  44196  areaquad  44410  imo72b2  45364  int-mulcomd  45368  int-rightdistd  45372  cvgdvgrat  45489  radcnvrat  45490  bccm1k  45518  binomcxplemwb  45524  binomcxplemnotnn0  45532  sineq0ALT  46110  mul13d  46501  divdiv3d  46576  mccllem  46814  coskpi2  47081  cosknegpi  47084  dvsinax  47128  dvasinbx  47135  dvcosax  47141  dvnxpaek  47157  dvnmul  47158  dvnprodlem2  47162  itgsinexplem1  47169  stoweidlem1  47216  stoweidlem11  47226  stoweidlem26  47241  stoweidlem32  47247  wallispilem4  47283  wallispi2lem1  47286  wallispi2lem2  47287  stirlinglem3  47291  stirlinglem4  47292  stirlinglem5  47293  stirlinglem7  47295  stirlinglem10  47298  stirlinglem15  47303  dirkertrigeqlem1  47313  dirkertrigeqlem2  47314  dirkertrigeqlem3  47315  dirkertrigeq  47316  dirkercncflem1  47318  fourierdlem16  47338  fourierdlem21  47343  fourierdlem22  47344  fourierdlem56  47377  fourierdlem66  47387  fourierdlem83  47404  fourierswlem  47445  fouriersw  47446  etransclem23  47472  etransclem24  47473  etransclem38  47487  etransclem46  47495  hoiprodp1  47803  hoidmvlelem2  47811  smfmullem1  48006  sigarac  48067  sigarls  48072  sigarid  48073  sigardiv  48076  sigarcol  48079  sigaradd  48081  cevathlem1  48082  sin3t  48122  cos3t  48123  sin5tlem1  48124  sin5tlem3  48126  sqrtnegnre  48582  fmtnoodd  48823  sqrtpwpw2p  48828  fmtnorec3  48838  fmtnoprmfac2lem1  48856  fmtnofac1  48860  lighneallem2  48896  lighneallem3  48897  proththd  48904  requad01  48924  dfeven2  48952  fppr2odd  49034  fpprwppr  49042  altgsumbc  49669  altgsumbcALT  49670  blennnt2  49906  dignn0flhalflem2  49933  dignn0ehalf  49934  itcovalt2lem2lem2  49991  affinecomb2  50020  rrx2linest  50059  itscnhlc0yqe  50076  itsclc0yqsollem1  50079  itscnhlc0xyqsol  50082  itschlc0xyqsol1  50083  itsclc0xyqsolr  50086  itsclquadb  50093  2itscplem3  50097  itscnhlinecirc02plem1  50099  itscnhlinecirc02plem2  50100  inlinecirc02p  50104  crosspaltd  51246  crossp3d  51247  amgmwlem  51267