Theorem mulcomd 11165

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 7368  ℂ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  11312  mul4r  11314  mulcand  11782  mulcan2d  11783  divcan1  11817  divrec2  11825  div23  11827  divdivdiv  11854  divmuleq  11858  divadddiv  11868  divcan5rd  11956  dmdcan2d  11959  mvllmuld  11985  rdiv  11988  subhalfhalf  12387  mul2lt0llt0  13023  mul2lt0lgt0  13024  prodge0ld  13027  xmulcom  13193  modvalr  13804  mulp1mod1  13846  modmul12d  13860  modnegd  13861  modmulmodr  13872  expaddz  14041  binom3  14159  expmulnbnd  14170  digit1  14172  bccmpl  14244  bcm1k  14250  bcn2  14254  bcpasc  14256  recval  15258  abs1m  15271  bhmafibid1cn  15401  bhmafibid2cn  15402  reccn2  15532  lo1mul2  15564  isummulc1  15698  fsummulc1  15720  incexclem  15771  incexc  15772  trireciplem  15797  pwdif  15803  geolim  15805  cvgrat  15818  mertens  15821  ntrivcvgmul  15837  fallfacfwd  15971  bpoly4  15994  fsumcube  15995  eftlub  16046  sinadd  16101  cosadd  16102  sin2t  16114  nndivides  16201  dvds2ln  16228  even2n  16281  oddm1even  16282  mod2eq1n2dvds  16286  m1exp1  16315  pwp1fsum  16330  divalgmod  16345  bitsp1  16370  bitsinv1lem  16380  sadadd2lem  16398  smumullem  16431  gcdmultiplez  16474  mulgcdr  16489  rplpwr  16497  lcmgcdlem  16545  divgcdcoprmex  16605  cncongr1  16606  eulerthlem2  16721  prmdiv  16724  prmdivdiv  16726  vfermltlALT  16742  modprmn0modprm0  16747  coprimeprodsq  16748  pythagtriplem6  16761  pythagtriplem7  16762  pceulem  16785  pcadd  16829  prmpwdvds  16844  mul4sqlem  16893  4sqlem17  16901  mulgassr  19054  odmodnn0  19481  odmulg  19497  odmulgeq  19498  odbezout  19499  odadd1  19789  ablfacrp2  20010  pgpfac1lem3  20020  zringlpirlem3  21431  znunit  21530  icopnfhmeo  24909  cphassr  25180  pjthlem1  25405  itgabs  25804  dvmulbr  25909  dvmulbrOLD  25910  dvcmul  25915  dvcmulf  25916  dvmptcmul  25936  cmvth  25963  cmvthOLD  25964  dvlipcn  25967  c1liplem1  25969  lhop1lem  25986  lhop2  25988  dvcvx  25993  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc1lem4  26014  itgparts  26022  dvply1  26259  elqaalem3  26297  aalioulem4  26311  taylthlem2  26350  taylthlem2OLD  26351  abelthlem6  26414  abelthlem7  26416  tangtx  26482  tanarg  26596  advlogexp  26632  mulcxp  26662  cxpmul  26665  abscxp  26669  dvcxp2  26718  cxpeq  26735  ang180lem1  26787  lawcoslem1  26793  lawcos  26794  heron  26816  dcubic1  26823  mcubic  26825  cubic2  26826  binom4  26828  dquart  26831  quart1lem  26833  quart1  26834  quartlem1  26835  dvatan  26913  leibpi  26920  log2cnv  26922  efrlim  26947  efrlimOLD  26948  cxp2lim  26955  cxploglim  26956  zetacvg  26993  lgamgulmlem2  27008  lgamgulmlem3  27009  wilthlem1  27046  ftalem1  27051  ftalem5  27055  basellem3  27061  basellem5  27063  mpodvdsmulf1o  27172  dvdsmulf1o  27174  sgmppw  27176  logfac2  27196  chpval2  27197  chpchtsum  27198  perfect1  27207  lgsdirprm  27310  lgsdi  27313  lgsdirnn0  27323  lgsdinn0  27324  gausslemma2dlem1a  27344  gausslemma2dlem6  27351  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  lgsquad2  27365  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgslem3d1  27382  2lgsoddprmlem2  27388  2sqlem3  27399  2sqlem4  27400  2sqmod  27415  chebbnd1lem2  27449  chebbnd1lem3  27450  chtppilimlem2  27453  chto1lb  27457  rplogsumlem1  27463  dchrisumlem2  27469  dchrvmasum2lem  27475  dchrisum0flblem2  27488  dchrisum0lem2a  27496  mulogsumlem  27510  mulog2sumlem2  27514  selberglem1  27524  selberg2lem  27529  selberg3lem1  27536  selberg4  27540  pntrsumo1  27544  selberg34r  27550  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntlemb  27576  pntlemq  27580  pntlemr  27581  pntlemj  27582  pntlemo  27586  pnt2  27592  pnt  27593  padicabvcxp  27611  ostth2lem2  27613  ostth2lem3  27614  ostth2lem4  27615  ttgcontlem1  28969  brbtwn2  28990  colinearalglem1  28991  colinearalg  28995  axpaschlem  29025  axcontlem8  29056  numclwwlk1  30448  numclwwlk7  30478  smcnlem  30784  pjhthlem1  31478  kbmul  32042  kbass2  32204  submuladdd  32829  muldivdid  32830  pythagreim  32835  quad3d  32839  sgnmul  32926  2exple2exp  32936  psgnfzto1st  33198  zringfrac  33646  ccfldextdgrr  33849  fldext2rspun  33859  fldext2chn  33905  constrrtlc1  33909  constrrtcclem  33911  constrrtcc  33912  constrremulcl  33944  constrmulcl  33948  cos9thpiminplylem1  33959  qqhval2lem  34158  qqhghm  34165  qqhrhm  34166  oddpwdc  34531  plymulx0  34724  signsvtp  34760  signsvtn  34761  signsvfpn  34762  signsvfnn  34763  breprexplemc  34809  circlemethhgt  34820  logdivsqrle  34827  hgt750lemf  34830  hgt750lemb  34833  hgt750leme  34835  subfacval2  35400  subfaclim  35401  fwddifnp1  36378  knoppndvlem11  36741  knoppndvlem17  36747  bj-subcom  37552  bj-bary1lem1  37555  itg2addnclem  37911  itg2addnclem2  37912  itgabsnc  37929  ftc1cnnclem  37931  areacirclem1  37948  areacirc  37953  geomcau  37999  bfplem1  38062  rrndstprj2  38071  rrnequiv  38075  lcmineqlem1  42388  lcmineqlem5  42392  lcmineqlem8  42395  lcmineqlem11  42398  lcmineqlem18  42405  lcmineqlem21  42408  3lexlogpow5ineq2  42414  3lexlogpow2ineq1  42417  dvrelogpow2b  42427  aks4d1p1p7  42433  primrootscoprmpow  42458  primrootscoprbij  42461  aks6d1c1  42475  aks6d1c2  42489  2np3bcnp1  42503  2ap1caineq  42504  bcle2d  42538  aks6d1c7lem1  42539  nicomachus  42671  retire  42678  readvrec  42721  3cubeslem2  43031  3cubeslem3l  43032  3cubeslem3r  43033  irrapxlem5  43172  pellexlem2  43176  pellexlem6  43180  qirropth  43254  rmxyadd  43267  rmxm1  43280  rmxluc  43282  rmyluc2  43284  rmydbl  43286  jm2.24nn  43305  jm2.17a  43306  jm2.17b  43307  jm2.17c  43308  jm2.18  43334  jm2.19lem2  43336  jm2.22  43341  jm2.23  43342  areaquad  43562  imo72b2  44517  int-mulcomd  44521  int-rightdistd  44525  cvgdvgrat  44658  radcnvrat  44659  bccm1k  44687  binomcxplemwb  44693  binomcxplemnotnn0  44701  sineq0ALT  45281  mul13d  45631  divdiv3d  45707  mccllem  45946  coskpi2  46213  cosknegpi  46216  dvsinax  46260  dvasinbx  46267  dvcosax  46273  dvnxpaek  46289  dvnmul  46290  dvnprodlem2  46294  itgsinexplem1  46301  stoweidlem1  46348  stoweidlem11  46358  stoweidlem26  46373  stoweidlem32  46379  wallispilem4  46415  wallispi2lem1  46418  wallispi2lem2  46419  stirlinglem3  46423  stirlinglem4  46424  stirlinglem5  46425  stirlinglem7  46427  stirlinglem10  46430  stirlinglem15  46435  dirkertrigeqlem1  46445  dirkertrigeqlem2  46446  dirkertrigeqlem3  46447  dirkertrigeq  46448  dirkercncflem1  46450  fourierdlem16  46470  fourierdlem21  46475  fourierdlem22  46476  fourierdlem56  46509  fourierdlem66  46519  fourierdlem83  46536  fourierswlem  46577  fouriersw  46578  etransclem23  46604  etransclem24  46605  etransclem38  46619  etransclem46  46627  hoiprodp1  46935  hoidmvlelem2  46943  smfmullem1  47138  sigarac  47199  sigarls  47204  sigarid  47205  sigardiv  47208  sigarcol  47211  sigaradd  47213  cevathlem1  47214  sqrtnegnre  47656  fmtnoodd  47882  sqrtpwpw2p  47887  fmtnorec3  47897  fmtnoprmfac2lem1  47915  fmtnofac1  47919  lighneallem2  47955  lighneallem3  47956  proththd  47963  requad01  47970  dfeven2  47998  fppr2odd  48080  fpprwppr  48088  altgsumbc  48701  altgsumbcALT  48702  blennnt2  48938  dignn0flhalflem2  48965  dignn0ehalf  48966  itcovalt2lem2lem2  49023  affinecomb2  49052  rrx2linest  49091  itscnhlc0yqe  49108  itsclc0yqsollem1  49111  itscnhlc0xyqsol  49114  itschlc0xyqsol1  49115  itsclc0xyqsolr  49118  itsclquadb  49125  2itscplem3  49129  itscnhlinecirc02plem1  49131  itscnhlinecirc02plem2  49132  inlinecirc02p  49136  amgmwlem  50150