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  28173  brbtwn2  28194  colinearalglem1  28195  colinearalg  28199  axpaschlem  28229  axcontlem8  28260  numclwwlk1  29645  numclwwlk7  29675  smcnlem  29981  pjhthlem1  30675  kbmul  31239  kbass2  31401  psgnfzto1st  32295  ccfldextdgrr  32777  qqhval2lem  32992  qqhghm  32999  qqhrhm  33000  oddpwdc  33384  sgnmul  33572  plymulx0  33589  signsvtp  33625  signsvtn  33626  signsvfpn  33627  signsvfnn  33628  breprexplemc  33675  circlemethhgt  33686  logdivsqrle  33693  hgt750lemf  33696  hgt750lemb  33699  hgt750leme  33701  subfacval2  34209  subfaclim  34210  fwddifnp1  35168  gg-dvmulbr  35206  gg-cmvth  35212  gg-dvfsumlem2  35214  knoppndvlem11  35446  knoppndvlem17  35452  bj-subcom  36237  bj-bary1lem1  36240  itg2addnclem  36587  itg2addnclem2  36588  itgabsnc  36605  ftc1cnnclem  36607  areacirclem1  36624  areacirc  36629  geomcau  36675  bfplem1  36738  rrndstprj2  36747  rrnequiv  36751  lcmineqlem1  40942  lcmineqlem5  40946  lcmineqlem8  40949  lcmineqlem11  40952  lcmineqlem18  40959  lcmineqlem21  40962  3lexlogpow5ineq2  40968  3lexlogpow2ineq1  40971  dvrelogpow2b  40981  aks4d1p1p7  40987  2np3bcnp1  41008  2ap1caineq  41009  nicomachus  41258  3cubeslem2  41471  3cubeslem3l  41472  3cubeslem3r  41473  irrapxlem5  41612  pellexlem2  41616  pellexlem6  41620  qirropth  41694  rmxyadd  41708  rmxm1  41721  rmxluc  41723  rmyluc2  41725  rmydbl  41727  jm2.24nn  41746  jm2.17a  41747  jm2.17b  41748  jm2.17c  41749  jm2.18  41775  jm2.19lem2  41777  jm2.22  41782  jm2.23  41783  areaquad  42013  imo72b2  42972  int-mulcomd  42976  int-rightdistd  42980  cvgdvgrat  43120  radcnvrat  43121  bccm1k  43149  binomcxplemwb  43155  binomcxplemnotnn0  43163  sineq0ALT  43746  mul13d  44037  divdiv3d  44117  mccllem  44361  coskpi2  44630  cosknegpi  44633  dvsinax  44677  dvasinbx  44684  dvcosax  44690  dvnxpaek  44706  dvnmul  44707  dvnprodlem2  44711  itgsinexplem1  44718  stoweidlem1  44765  stoweidlem11  44775  stoweidlem26  44790  stoweidlem32  44796  wallispilem4  44832  wallispi2lem1  44835  wallispi2lem2  44836  stirlinglem3  44840  stirlinglem4  44841  stirlinglem5  44842  stirlinglem7  44844  stirlinglem10  44847  stirlinglem15  44852  dirkertrigeqlem1  44862  dirkertrigeqlem2  44863  dirkertrigeqlem3  44864  dirkertrigeq  44865  dirkercncflem1  44867  fourierdlem16  44887  fourierdlem21  44892  fourierdlem22  44893  fourierdlem56  44926  fourierdlem66  44936  fourierdlem83  44953  fourierswlem  44994  fouriersw  44995  etransclem23  45021  etransclem24  45022  etransclem38  45036  etransclem46  45044  hoiprodp1  45352  hoidmvlelem2  45360  smfmullem1  45555  sigarac  45616  sigarls  45621  sigarid  45622  sigardiv  45625  sigarcol  45628  sigaradd  45630  cevathlem1  45631  sqrtnegnre  46063  fmtnoodd  46249  sqrtpwpw2p  46254  fmtnorec3  46264  fmtnoprmfac2lem1  46282  fmtnofac1  46286  lighneallem2  46322  lighneallem3  46323  proththd  46330  requad01  46337  dfeven2  46365  fppr2odd  46447  fpprwppr  46455  altgsumbc  47076  altgsumbcALT  47077  blennnt2  47323  dignn0flhalflem2  47350  dignn0ehalf  47351  itcovalt2lem2lem2  47408  affinecomb2  47437  rrx2linest  47476  itscnhlc0yqe  47493  itsclc0yqsollem1  47496  itscnhlc0xyqsol  47499  itschlc0xyqsol1  47500  itsclc0xyqsolr  47503  itsclquadb  47510  2itscplem3  47514  itscnhlinecirc02plem1  47516  itscnhlinecirc02plem2  47517  inlinecirc02p  47521  amgmwlem  47897