Theorem mulcomd 11164

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  mul31  11311  mul4r  11313  mulcand  11781  mulcan2d  11782  divcan1  11816  divrec2  11824  div23  11826  muldivdid  11847  divdivdiv  11854  divmuleq  11858  divadddiv  11868  divcan5rd  11956  dmdcan2d  11959  mvllmuld  11985  rdiv  11988  subhalfhalf  12409  mul2lt0llt0  13046  mul2lt0lgt0  13047  prodge0ld  13050  xmulcom  13216  modvalr  13829  mulp1mod1  13871  modmul12d  13885  modnegd  13886  modmulmodr  13897  expaddz  14066  binom3  14184  expmulnbnd  14195  digit1  14197  bccmpl  14269  bcm1k  14275  bcn2  14279  bcpasc  14281  recval  15283  abs1m  15296  bhmafibid1cn  15426  bhmafibid2cn  15427  reccn2  15557  lo1mul2  15589  isummulc1  15723  fsummulc1  15745  incexclem  15799  incexc  15800  trireciplem  15825  pwdif  15831  geolim  15833  cvgrat  15846  mertens  15849  ntrivcvgmul  15865  fallfacfwd  15999  bpoly4  16022  fsumcube  16023  eftlub  16074  sinadd  16129  cosadd  16130  sin2t  16142  nndivides  16229  dvds2ln  16256  even2n  16309  oddm1even  16310  mod2eq1n2dvds  16314  m1exp1  16343  pwp1fsum  16358  divalgmod  16373  bitsp1  16398  bitsinv1lem  16408  sadadd2lem  16426  smumullem  16459  gcdmultiplez  16502  mulgcdr  16517  rplpwr  16525  lcmgcdlem  16573  divgcdcoprmex  16633  cncongr1  16634  eulerthlem2  16750  prmdiv  16753  prmdivdiv  16755  vfermltlALT  16771  modprmn0modprm0  16776  coprimeprodsq  16777  pythagtriplem6  16790  pythagtriplem7  16791  pceulem  16814  pcadd  16858  prmpwdvds  16873  mul4sqlem  16922  4sqlem17  16930  mulgassr  19086  odmodnn0  19513  odmulg  19529  odmulgeq  19530  odbezout  19531  odadd1  19821  ablfacrp2  20042  pgpfac1lem3  20052  zringlpirlem3  21446  znunit  21545  icopnfhmeo  24935  cphassr  25204  pjthlem1  25429  itgabs  25827  dvmulbr  25931  dvcmul  25936  dvcmulf  25937  dvmptcmul  25956  cmvth  25983  dvlipcn  25986  c1liplem1  25988  lhop1lem  26005  lhop2  26007  dvcvx  26012  dvfsumlem2  26019  ftc1lem4  26031  itgparts  26039  dvply1  26275  elqaalem3  26312  aalioulem4  26326  taylthlem2  26364  abelthlem6  26426  abelthlem7  26428  tangtx  26494  tanarg  26608  advlogexp  26644  mulcxp  26674  cxpmul  26677  abscxp  26681  dvcxp2  26730  cxpeq  26746  ang180lem1  26798  lawcoslem1  26804  lawcos  26805  heron  26827  dcubic1  26834  mcubic  26836  cubic2  26837  binom4  26839  dquart  26842  quart1lem  26844  quart1  26845  quartlem1  26846  dvatan  26924  leibpi  26931  log2cnv  26933  efrlim  26958  cxp2lim  26965  cxploglim  26966  zetacvg  27003  lgamgulmlem2  27018  lgamgulmlem3  27019  wilthlem1  27056  ftalem1  27061  ftalem5  27065  basellem3  27071  basellem5  27073  mpodvdsmulf1o  27182  dvdsmulf1o  27184  sgmppw  27185  logfac2  27205  chpval2  27206  chpchtsum  27207  perfect1  27216  lgsdirprm  27319  lgsdi  27322  lgsdirnn0  27332  lgsdinn0  27333  gausslemma2dlem1a  27353  gausslemma2dlem6  27360  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  lgsquad2  27374  2lgslem3a1  27388  2lgslem3b1  27389  2lgslem3c1  27390  2lgslem3d1  27391  2lgsoddprmlem2  27397  2sqlem3  27408  2sqlem4  27409  2sqmod  27424  chebbnd1lem2  27458  chebbnd1lem3  27459  chtppilimlem2  27462  chto1lb  27466  rplogsumlem1  27472  dchrisumlem2  27478  dchrvmasum2lem  27484  dchrisum0flblem2  27497  dchrisum0lem2a  27505  mulogsumlem  27519  mulog2sumlem2  27523  selberglem1  27533  selberg2lem  27538  selberg3lem1  27545  selberg4  27549  pntrsumo1  27553  selberg34r  27559  pntrlog2bndlem3  27567  pntrlog2bndlem4  27568  pntlemb  27585  pntlemq  27589  pntlemr  27590  pntlemj  27591  pntlemo  27595  pnt2  27601  pnt  27602  padicabvcxp  27620  ostth2lem2  27622  ostth2lem3  27623  ostth2lem4  27624  ttgcontlem1  28978  brbtwn2  28999  colinearalglem1  29000  colinearalg  29004  axpaschlem  29034  axcontlem8  29065  numclwwlk1  30456  numclwwlk7  30486  smcnlem  30793  pjhthlem1  31487  kbmul  32051  kbass2  32213  submuladdd  32839  pythagreim  32844  quad3d  32848  sgnmul  32934  2exple2exp  32944  psgnfzto1st  33193  zringfrac  33644  ccfldextdgrr  33863  fldext2rspun  33873  fldext2chn  33919  constrrtlc1  33923  constrrtcclem  33925  constrrtcc  33926  constrremulcl  33958  constrmulcl  33962  cos9thpiminplylem1  33973  qqhval2lem  34172  qqhghm  34179  qqhrhm  34180  oddpwdc  34545  plymulx0  34738  signsvtp  34774  signsvtn  34775  signsvfpn  34776  signsvfnn  34777  breprexplemc  34823  circlemethhgt  34834  logdivsqrle  34841  hgt750lemf  34844  hgt750lemb  34847  hgt750leme  34849  subfacval2  35416  subfaclim  35417  fwddifnp1  36394  knoppndvlem11  36829  knoppndvlem17  36835  bj-subcom  37669  bj-bary1lem1  37672  itg2addnclem  38039  itg2addnclem2  38040  itgabsnc  38057  ftc1cnnclem  38059  areacirclem1  38076  areacirc  38081  geomcau  38127  bfplem1  38190  rrndstprj2  38199  rrnequiv  38203  lcmineqlem1  42515  lcmineqlem5  42519  lcmineqlem8  42522  lcmineqlem11  42525  lcmineqlem18  42532  lcmineqlem21  42535  3lexlogpow5ineq2  42541  3lexlogpow2ineq1  42544  dvrelogpow2b  42554  aks4d1p1p7  42560  primrootscoprmpow  42585  primrootscoprbij  42588  aks6d1c1  42602  aks6d1c2  42616  2np3bcnp1  42630  2ap1caineq  42631  bcle2d  42665  aks6d1c7lem1  42666  nicomachus  42790  retire  42797  readvrec  42840  3cubeslem2  43135  3cubeslem3l  43136  3cubeslem3r  43137  irrapxlem5  43272  pellexlem2  43276  pellexlem6  43280  qirropth  43354  rmxyadd  43367  rmxm1  43380  rmxluc  43382  rmyluc2  43384  rmydbl  43386  jm2.24nn  43405  jm2.17a  43406  jm2.17b  43407  jm2.17c  43408  jm2.18  43434  jm2.19lem2  43436  jm2.22  43441  jm2.23  43442  areaquad  43662  imo72b2  44617  int-mulcomd  44621  int-rightdistd  44625  cvgdvgrat  44758  radcnvrat  44759  bccm1k  44787  binomcxplemwb  44793  binomcxplemnotnn0  44801  sineq0ALT  45381  mul13d  45729  divdiv3d  45805  mccllem  46043  coskpi2  46310  cosknegpi  46313  dvsinax  46357  dvasinbx  46364  dvcosax  46370  dvnxpaek  46386  dvnmul  46387  dvnprodlem2  46391  itgsinexplem1  46398  stoweidlem1  46445  stoweidlem11  46455  stoweidlem26  46470  stoweidlem32  46476  wallispilem4  46512  wallispi2lem1  46515  wallispi2lem2  46516  stirlinglem3  46520  stirlinglem4  46521  stirlinglem5  46522  stirlinglem7  46524  stirlinglem10  46527  stirlinglem15  46532  dirkertrigeqlem1  46542  dirkertrigeqlem2  46543  dirkertrigeqlem3  46544  dirkertrigeq  46545  dirkercncflem1  46547  fourierdlem16  46567  fourierdlem21  46572  fourierdlem22  46573  fourierdlem56  46606  fourierdlem66  46616  fourierdlem83  46633  fourierswlem  46674  fouriersw  46675  etransclem23  46701  etransclem24  46702  etransclem38  46716  etransclem46  46724  hoiprodp1  47032  hoidmvlelem2  47040  smfmullem1  47235  sigarac  47296  sigarls  47301  sigarid  47302  sigardiv  47305  sigarcol  47308  sigaradd  47310  cevathlem1  47311  sin3t  47335  cos3t  47336  sin5tlem1  47337  sin5tlem3  47339  sqrtnegnre  47771  fmtnoodd  48012  sqrtpwpw2p  48017  fmtnorec3  48027  fmtnoprmfac2lem1  48045  fmtnofac1  48049  lighneallem2  48085  lighneallem3  48086  proththd  48093  requad01  48113  dfeven2  48141  fppr2odd  48223  fpprwppr  48231  altgsumbc  48844  altgsumbcALT  48845  blennnt2  49081  dignn0flhalflem2  49108  dignn0ehalf  49109  itcovalt2lem2lem2  49166  affinecomb2  49195  rrx2linest  49234  itscnhlc0yqe  49251  itsclc0yqsollem1  49254  itscnhlc0xyqsol  49257  itschlc0xyqsol1  49258  itsclc0xyqsolr  49261  itsclquadb  49268  2itscplem3  49272  itscnhlinecirc02plem1  49274  itscnhlinecirc02plem2  49275  inlinecirc02p  49279  amgmwlem  50293