Theorem mulcomd 11157

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028   · cmul 11035

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

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

This theorem is referenced by:  mul31  11304  mul4r  11306  mulcand  11774  mulcan2d  11775  divcan1  11809  divrec2  11817  div23  11819  divdivdiv  11846  divmuleq  11850  divadddiv  11860  divcan5rd  11948  dmdcan2d  11951  mvllmuld  11977  rdiv  11980  subhalfhalf  12379  mul2lt0llt0  13015  mul2lt0lgt0  13016  prodge0ld  13019  xmulcom  13185  modvalr  13796  mulp1mod1  13838  modmul12d  13852  modnegd  13853  modmulmodr  13864  expaddz  14033  binom3  14151  expmulnbnd  14162  digit1  14164  bccmpl  14236  bcm1k  14242  bcn2  14246  bcpasc  14248  recval  15250  abs1m  15263  bhmafibid1cn  15393  bhmafibid2cn  15394  reccn2  15524  lo1mul2  15556  isummulc1  15690  fsummulc1  15712  incexclem  15763  incexc  15764  trireciplem  15789  pwdif  15795  geolim  15797  cvgrat  15810  mertens  15813  ntrivcvgmul  15829  fallfacfwd  15963  bpoly4  15986  fsumcube  15987  eftlub  16038  sinadd  16093  cosadd  16094  sin2t  16106  nndivides  16193  dvds2ln  16220  even2n  16273  oddm1even  16274  mod2eq1n2dvds  16278  m1exp1  16307  pwp1fsum  16322  divalgmod  16337  bitsp1  16362  bitsinv1lem  16372  sadadd2lem  16390  smumullem  16423  gcdmultiplez  16466  mulgcdr  16481  rplpwr  16489  lcmgcdlem  16537  divgcdcoprmex  16597  cncongr1  16598  eulerthlem2  16713  prmdiv  16716  prmdivdiv  16718  vfermltlALT  16734  modprmn0modprm0  16739  coprimeprodsq  16740  pythagtriplem6  16753  pythagtriplem7  16754  pceulem  16777  pcadd  16821  prmpwdvds  16836  mul4sqlem  16885  4sqlem17  16893  mulgassr  19046  odmodnn0  19473  odmulg  19489  odmulgeq  19490  odbezout  19491  odadd1  19781  ablfacrp2  20002  pgpfac1lem3  20012  zringlpirlem3  21423  znunit  21522  icopnfhmeo  24901  cphassr  25172  pjthlem1  25397  itgabs  25796  dvmulbr  25901  dvmulbrOLD  25902  dvcmul  25907  dvcmulf  25908  dvmptcmul  25928  cmvth  25955  cmvthOLD  25956  dvlipcn  25959  c1liplem1  25961  lhop1lem  25978  lhop2  25980  dvcvx  25985  dvfsumlem2  25993  dvfsumlem2OLD  25994  ftc1lem4  26006  itgparts  26014  dvply1  26251  elqaalem3  26289  aalioulem4  26303  taylthlem2  26342  taylthlem2OLD  26343  abelthlem6  26406  abelthlem7  26408  tangtx  26474  tanarg  26588  advlogexp  26624  mulcxp  26654  cxpmul  26657  abscxp  26661  dvcxp2  26710  cxpeq  26727  ang180lem1  26779  lawcoslem1  26785  lawcos  26786  heron  26808  dcubic1  26815  mcubic  26817  cubic2  26818  binom4  26820  dquart  26823  quart1lem  26825  quart1  26826  quartlem1  26827  dvatan  26905  leibpi  26912  log2cnv  26914  efrlim  26939  efrlimOLD  26940  cxp2lim  26947  cxploglim  26948  zetacvg  26985  lgamgulmlem2  27000  lgamgulmlem3  27001  wilthlem1  27038  ftalem1  27043  ftalem5  27047  basellem3  27053  basellem5  27055  mpodvdsmulf1o  27164  dvdsmulf1o  27166  sgmppw  27168  logfac2  27188  chpval2  27189  chpchtsum  27190  perfect1  27199  lgsdirprm  27302  lgsdi  27305  lgsdirnn0  27315  lgsdinn0  27316  gausslemma2dlem1a  27336  gausslemma2dlem6  27343  lgsquadlem1  27351  lgsquadlem2  27352  lgsquadlem3  27353  lgsquad2  27357  2lgslem3a1  27371  2lgslem3b1  27372  2lgslem3c1  27373  2lgslem3d1  27374  2lgsoddprmlem2  27380  2sqlem3  27391  2sqlem4  27392  2sqmod  27407  chebbnd1lem2  27441  chebbnd1lem3  27442  chtppilimlem2  27445  chto1lb  27449  rplogsumlem1  27455  dchrisumlem2  27461  dchrvmasum2lem  27467  dchrisum0flblem2  27480  dchrisum0lem2a  27488  mulogsumlem  27502  mulog2sumlem2  27506  selberglem1  27516  selberg2lem  27521  selberg3lem1  27528  selberg4  27532  pntrsumo1  27536  selberg34r  27542  pntrlog2bndlem3  27550  pntrlog2bndlem4  27551  pntlemb  27568  pntlemq  27572  pntlemr  27573  pntlemj  27574  pntlemo  27578  pnt2  27584  pnt  27585  padicabvcxp  27603  ostth2lem2  27605  ostth2lem3  27606  ostth2lem4  27607  ttgcontlem1  28940  brbtwn2  28961  colinearalglem1  28962  colinearalg  28966  axpaschlem  28996  axcontlem8  29027  numclwwlk1  30419  numclwwlk7  30449  smcnlem  30755  pjhthlem1  31449  kbmul  32013  kbass2  32175  submuladdd  32800  muldivdid  32801  pythagreim  32806  quad3d  32810  sgnmul  32897  2exple2exp  32907  psgnfzto1st  33168  zringfrac  33616  ccfldextdgrr  33810  fldext2rspun  33820  fldext2chn  33866  constrrtlc1  33870  constrrtcclem  33872  constrrtcc  33873  constrremulcl  33905  constrmulcl  33909  cos9thpiminplylem1  33920  qqhval2lem  34119  qqhghm  34126  qqhrhm  34127  oddpwdc  34492  plymulx0  34685  signsvtp  34721  signsvtn  34722  signsvfpn  34723  signsvfnn  34724  breprexplemc  34770  circlemethhgt  34781  logdivsqrle  34788  hgt750lemf  34791  hgt750lemb  34794  hgt750leme  34796  subfacval2  35362  subfaclim  35363  fwddifnp1  36340  knoppndvlem11  36697  knoppndvlem17  36703  bj-subcom  37484  bj-bary1lem1  37487  itg2addnclem  37843  itg2addnclem2  37844  itgabsnc  37861  ftc1cnnclem  37863  areacirclem1  37880  areacirc  37885  geomcau  37931  bfplem1  37994  rrndstprj2  38003  rrnequiv  38007  lcmineqlem1  42320  lcmineqlem5  42324  lcmineqlem8  42327  lcmineqlem11  42330  lcmineqlem18  42337  lcmineqlem21  42340  3lexlogpow5ineq2  42346  3lexlogpow2ineq1  42349  dvrelogpow2b  42359  aks4d1p1p7  42365  primrootscoprmpow  42390  primrootscoprbij  42393  aks6d1c1  42407  aks6d1c2  42421  2np3bcnp1  42435  2ap1caineq  42436  bcle2d  42470  aks6d1c7lem1  42471  nicomachus  42603  retire  42610  readvrec  42653  3cubeslem2  42963  3cubeslem3l  42964  3cubeslem3r  42965  irrapxlem5  43104  pellexlem2  43108  pellexlem6  43112  qirropth  43186  rmxyadd  43199  rmxm1  43212  rmxluc  43214  rmyluc2  43216  rmydbl  43218  jm2.24nn  43237  jm2.17a  43238  jm2.17b  43239  jm2.17c  43240  jm2.18  43266  jm2.19lem2  43268  jm2.22  43273  jm2.23  43274  areaquad  43494  imo72b2  44449  int-mulcomd  44453  int-rightdistd  44457  cvgdvgrat  44590  radcnvrat  44591  bccm1k  44619  binomcxplemwb  44625  binomcxplemnotnn0  44633  sineq0ALT  45213  mul13d  45564  divdiv3d  45640  mccllem  45879  coskpi2  46146  cosknegpi  46149  dvsinax  46193  dvasinbx  46200  dvcosax  46206  dvnxpaek  46222  dvnmul  46223  dvnprodlem2  46227  itgsinexplem1  46234  stoweidlem1  46281  stoweidlem11  46291  stoweidlem26  46306  stoweidlem32  46312  wallispilem4  46348  wallispi2lem1  46351  wallispi2lem2  46352  stirlinglem3  46356  stirlinglem4  46357  stirlinglem5  46358  stirlinglem7  46360  stirlinglem10  46363  stirlinglem15  46368  dirkertrigeqlem1  46378  dirkertrigeqlem2  46379  dirkertrigeqlem3  46380  dirkertrigeq  46381  dirkercncflem1  46383  fourierdlem16  46403  fourierdlem21  46408  fourierdlem22  46409  fourierdlem56  46442  fourierdlem66  46452  fourierdlem83  46469  fourierswlem  46510  fouriersw  46511  etransclem23  46537  etransclem24  46538  etransclem38  46552  etransclem46  46560  hoiprodp1  46868  hoidmvlelem2  46876  smfmullem1  47071  sigarac  47132  sigarls  47137  sigarid  47138  sigardiv  47141  sigarcol  47144  sigaradd  47146  cevathlem1  47147  sqrtnegnre  47589  fmtnoodd  47815  sqrtpwpw2p  47820  fmtnorec3  47830  fmtnoprmfac2lem1  47848  fmtnofac1  47852  lighneallem2  47888  lighneallem3  47889  proththd  47896  requad01  47903  dfeven2  47931  fppr2odd  48013  fpprwppr  48021  altgsumbc  48634  altgsumbcALT  48635  blennnt2  48871  dignn0flhalflem2  48898  dignn0ehalf  48899  itcovalt2lem2lem2  48956  affinecomb2  48985  rrx2linest  49024  itscnhlc0yqe  49041  itsclc0yqsollem1  49044  itscnhlc0xyqsol  49047  itschlc0xyqsol1  49048  itsclc0xyqsolr  49051  itsclquadb  49058  2itscplem3  49062  itscnhlinecirc02plem1  49064  itscnhlinecirc02plem2  49065  inlinecirc02p  49069  amgmwlem  50083