Theorem mulcomd 11235

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

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

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  mul31  11381  mul4r  11383  mulcand  11847  mulcan2d  11848  divcan1  11881  divrec2  11889  div23  11891  divdivdiv  11915  divmuleq  11919  divadddiv  11929  divcan5rd  12017  dmdcan2d  12020  mvllmuld  12046  rdiv  12049  subhalfhalf  12446  mul2lt0llt0  13078  mul2lt0lgt0  13079  prodge0ld  13082  xmulcom  13245  modvalr  13837  mulp1mod1  13877  modmul12d  13890  modnegd  13891  modmulmodr  13902  expaddz  14072  binom3  14187  expmulnbnd  14198  digit1  14200  bccmpl  14269  bcm1k  14275  bcn2  14279  bcpasc  14281  recval  15269  abs1m  15282  bhmafibid1cn  15410  bhmafibid2cn  15411  reccn2  15541  lo1mul2  15573  isummulc1  15709  fsummulc1  15731  incexclem  15782  incexc  15783  trireciplem  15808  pwdif  15814  geolim  15816  cvgrat  15829  mertens  15832  ntrivcvgmul  15848  fallfacfwd  15980  bpoly4  16003  fsumcube  16004  eftlub  16052  sinadd  16107  cosadd  16108  sin2t  16120  nndivides  16207  dvds2ln  16232  even2n  16285  oddm1even  16286  mod2eq1n2dvds  16290  m1exp1  16319  pwp1fsum  16334  divalgmod  16349  bitsp1  16372  bitsinv1lem  16382  sadadd2lem  16400  smumullem  16433  gcdmultiplez  16477  mulgcdr  16492  rplpwr  16499  lcmgcdlem  16543  divgcdcoprmex  16603  cncongr1  16604  eulerthlem2  16715  prmdiv  16718  prmdivdiv  16720  vfermltlALT  16735  modprmn0modprm0  16740  coprimeprodsq  16741  pythagtriplem6  16754  pythagtriplem7  16755  pceulem  16778  pcadd  16822  prmpwdvds  16837  mul4sqlem  16886  4sqlem17  16894  mulgassr  18992  odmodnn0  19408  odmulg  19424  odmulgeq  19425  odbezout  19426  odadd1  19716  ablfacrp2  19937  pgpfac1lem3  19947  zringlpirlem3  21034  znunit  21119  icopnfhmeo  24459  cphassr  24729  pjthlem1  24954  itgabs  25352  dvmulbr  25456  dvcmul  25461  dvcmulf  25462  dvmptcmul  25481  cmvth  25508  dvlipcn  25511  c1liplem1  25513  lhop1lem  25530  lhop2  25532  dvcvx  25537  dvfsumlem2  25544  ftc1lem4  25556  itgparts  25564  dvply1  25797  elqaalem3  25834  aalioulem4  25848  taylthlem2  25886  abelthlem6  25948  abelthlem7  25950  tangtx  26015  tanarg  26127  advlogexp  26163  mulcxp  26193  cxpmul  26196  abscxp  26200  dvcxp2  26249  cxpeq  26265  ang180lem1  26314  lawcoslem1  26320  lawcos  26321  heron  26343  dcubic1  26350  mcubic  26352  cubic2  26353  binom4  26355  dquart  26358  quart1lem  26360  quart1  26361  quartlem1  26362  dvatan  26440  leibpi  26447  log2cnv  26449  efrlim  26474  cxp2lim  26481  cxploglim  26482  zetacvg  26519  lgamgulmlem2  26534  lgamgulmlem3  26535  wilthlem1  26572  ftalem1  26577  ftalem5  26581  basellem3  26587  basellem5  26589  dvdsmulf1o  26698  sgmppw  26700  logfac2  26720  chpval2  26721  chpchtsum  26722  perfect1  26731  lgsdirprm  26834  lgsdi  26837  lgsdirnn0  26847  lgsdinn0  26848  gausslemma2dlem1a  26868  gausslemma2dlem6  26875  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  lgsquad2  26889  2lgslem3a1  26903  2lgslem3b1  26904  2lgslem3c1  26905  2lgslem3d1  26906  2lgsoddprmlem2  26912  2sqlem3  26923  2sqlem4  26924  2sqmod  26939  chebbnd1lem2  26973  chebbnd1lem3  26974  chtppilimlem2  26977  chto1lb  26981  rplogsumlem1  26987  dchrisumlem2  26993  dchrvmasum2lem  26999  dchrisum0flblem2  27012  dchrisum0lem2a  27020  mulogsumlem  27034  mulog2sumlem2  27038  selberglem1  27048  selberg2lem  27053  selberg3lem1  27060  selberg4  27064  pntrsumo1  27068  selberg34r  27074  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntlemb  27100  pntlemq  27104  pntlemr  27105  pntlemj  27106  pntlemo  27110  pnt2  27116  pnt  27117  padicabvcxp  27135  ostth2lem2  27137  ostth2lem3  27138  ostth2lem4  27139  ttgcontlem1  28142  brbtwn2  28163  colinearalglem1  28164  colinearalg  28168  axpaschlem  28198  axcontlem8  28229  numclwwlk1  29614  numclwwlk7  29644  smcnlem  29950  pjhthlem1  30644  kbmul  31208  kbass2  31370  psgnfzto1st  32264  ccfldextdgrr  32746  qqhval2lem  32961  qqhghm  32968  qqhrhm  32969  oddpwdc  33353  sgnmul  33541  plymulx0  33558  signsvtp  33594  signsvtn  33595  signsvfpn  33596  signsvfnn  33597  breprexplemc  33644  circlemethhgt  33655  logdivsqrle  33662  hgt750lemf  33665  hgt750lemb  33668  hgt750leme  33670  subfacval2  34178  subfaclim  34179  fwddifnp1  35137  gg-dvmulbr  35175  gg-cmvth  35181  gg-dvfsumlem2  35183  knoppndvlem11  35398  knoppndvlem17  35404  bj-subcom  36189  bj-bary1lem1  36192  itg2addnclem  36539  itg2addnclem2  36540  itgabsnc  36557  ftc1cnnclem  36559  areacirclem1  36576  areacirc  36581  geomcau  36627  bfplem1  36690  rrndstprj2  36699  rrnequiv  36703  lcmineqlem1  40894  lcmineqlem5  40898  lcmineqlem8  40901  lcmineqlem11  40904  lcmineqlem18  40911  lcmineqlem21  40914  3lexlogpow5ineq2  40920  3lexlogpow2ineq1  40923  dvrelogpow2b  40933  aks4d1p1p7  40939  2np3bcnp1  40960  2ap1caineq  40961  nicomachus  41210  3cubeslem2  41423  3cubeslem3l  41424  3cubeslem3r  41425  irrapxlem5  41564  pellexlem2  41568  pellexlem6  41572  qirropth  41646  rmxyadd  41660  rmxm1  41673  rmxluc  41675  rmyluc2  41677  rmydbl  41679  jm2.24nn  41698  jm2.17a  41699  jm2.17b  41700  jm2.17c  41701  jm2.18  41727  jm2.19lem2  41729  jm2.22  41734  jm2.23  41735  areaquad  41965  imo72b2  42924  int-mulcomd  42928  int-rightdistd  42932  cvgdvgrat  43072  radcnvrat  43073  bccm1k  43101  binomcxplemwb  43107  binomcxplemnotnn0  43115  sineq0ALT  43698  mul13d  43989  divdiv3d  44069  mccllem  44313  coskpi2  44582  cosknegpi  44585  dvsinax  44629  dvasinbx  44636  dvcosax  44642  dvnxpaek  44658  dvnmul  44659  dvnprodlem2  44663  itgsinexplem1  44670  stoweidlem1  44717  stoweidlem11  44727  stoweidlem26  44742  stoweidlem32  44748  wallispilem4  44784  wallispi2lem1  44787  wallispi2lem2  44788  stirlinglem3  44792  stirlinglem4  44793  stirlinglem5  44794  stirlinglem7  44796  stirlinglem10  44799  stirlinglem15  44804  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkercncflem1  44819  fourierdlem16  44839  fourierdlem21  44844  fourierdlem22  44845  fourierdlem56  44878  fourierdlem66  44888  fourierdlem83  44905  fourierswlem  44946  fouriersw  44947  etransclem23  44973  etransclem24  44974  etransclem38  44988  etransclem46  44996  hoiprodp1  45304  hoidmvlelem2  45312  smfmullem1  45507  sigarac  45568  sigarls  45573  sigarid  45574  sigardiv  45577  sigarcol  45580  sigaradd  45582  cevathlem1  45583  sqrtnegnre  46015  fmtnoodd  46201  sqrtpwpw2p  46206  fmtnorec3  46216  fmtnoprmfac2lem1  46234  fmtnofac1  46238  lighneallem2  46274  lighneallem3  46275  proththd  46282  requad01  46289  dfeven2  46317  fppr2odd  46399  fpprwppr  46407  altgsumbc  47028  altgsumbcALT  47029  blennnt2  47275  dignn0flhalflem2  47302  dignn0ehalf  47303  itcovalt2lem2lem2  47360  affinecomb2  47389  rrx2linest  47428  itscnhlc0yqe  47445  itsclc0yqsollem1  47448  itscnhlc0xyqsol  47451  itschlc0xyqsol1  47452  itsclc0xyqsolr  47455  itsclquadb  47462  2itscplem3  47466  itscnhlinecirc02plem1  47468  itscnhlinecirc02plem2  47469  inlinecirc02p  47473  amgmwlem  47849