Theorem mulcomd 9940

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  mul31  10083  subdir2d  10367  mulcand  10539  mulcan2d  10540  divcan1  10573  divrec2  10581  div23  10583  divdivdiv  10605  divmuleq  10609  divadddiv  10619  divcan5rd  10707  dmdcan2d  10710  mvllmuld  10736  subhalfhalf  11143  mul2lt0llt0  11810  mul2lt0lgt0  11811  xmulcom  11968  modvalr  12533  mulp1mod1  12573  modmul12d  12586  modnegd  12587  modmulmodr  12598  expaddz  12766  binom3  12847  expmulnbnd  12858  digit1  12860  bccmpl  12958  bcm1k  12964  bcn2  12968  bcpasc  12970  recval  13910  abs1m  13923  reccn2  14175  lo1mul2  14207  isummulc1  14336  fsummulc1  14359  incexclem  14407  incexc  14408  trireciplem  14433  geolim  14440  cvgrat  14454  mertens  14457  ntrivcvgmul  14473  fallfacfwd  14606  bpoly4  14629  fsumcube  14630  eftlub  14678  sinadd  14733  cosadd  14734  sin2t  14746  nndivides  14828  dvds2ln  14852  even2n  14904  oddm1even  14905  mod2eq1n2dvds  14909  m1exp1  14931  pwp1fsum  14952  divalgmod  14967  divalgmodOLD  14968  bitsp1  14991  bitsinv1lem  15001  sadadd2lem  15019  smumullem  15052  mulgcdr  15105  rplpwr  15114  lcmgcdlem  15157  divgcdcoprmex  15218  cncongr1  15219  eulerthlem2  15325  prmdiv  15328  prmdivdiv  15330  vfermltlALT  15345  modprmn0modprm0  15350  coprimeprodsq  15351  pythagtriplem6  15364  pythagtriplem7  15365  pceulem  15388  pcadd  15431  prmpwdvds  15446  mul4sqlem  15495  4sqlem17  15503  mulgassr  17403  odmodnn0  17782  odmulg  17796  odmulgeq  17797  odbezout  17798  odadd1  18074  ablfacrp2  18289  pgpfac1lem3  18299  zringlpirlem3  19653  znunit  19731  icopnfhmeo  22550  cphassr  22820  pjthlem1  23016  itgabs  23407  dvmulbr  23508  dvcmul  23513  dvcmulf  23514  dvmptcmul  23533  cmvth  23558  dvlipcn  23561  c1liplem1  23563  lhop1lem  23580  lhop2  23582  dvcvx  23587  dvfsumlem2  23594  ftc1lem4  23606  itgparts  23614  dvply1  23843  elqaalem3  23880  aalioulem4  23894  taylthlem2  23932  abelthlem6  23994  abelthlem7  23996  tangtx  24061  tanarg  24169  advlogexp  24201  mulcxp  24231  cxpmul  24234  abscxp  24238  dvcxp2  24282  cxpeq  24298  ang180lem1  24339  lawcoslem1  24345  lawcos  24346  heron  24365  dcubic1  24372  mcubic  24374  cubic2  24375  binom4  24377  dquart  24380  quart1lem  24382  quart1  24383  quartlem1  24384  dvatan  24462  leibpi  24469  log2cnv  24471  efrlim  24496  cxp2lim  24503  cxploglim  24504  zetacvg  24541  lgamgulmlem2  24556  lgamgulmlem3  24557  wilthlem1  24594  ftalem1  24599  ftalem5  24603  basellem3  24609  basellem5  24611  dvdsmulf1o  24720  sgmppw  24722  logfac2  24742  chpval2  24743  chpchtsum  24744  perfect1  24753  lgsdirprm  24856  lgsdi  24859  lgsdirnn0  24869  lgsdinn0  24870  gausslemma2dlem1a  24890  gausslemma2dlem6  24897  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2  24911  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgslem3d1  24928  2lgsoddprmlem2  24934  2sqlem3  24945  2sqlem4  24946  chebbnd1lem2  24959  chebbnd1lem3  24960  chtppilimlem2  24963  chto1lb  24967  rplogsumlem1  24973  dchrisumlem2  24979  dchrvmasum2lem  24985  dchrisum0flblem2  24998  dchrisum0lem2a  25006  mulogsumlem  25020  mulog2sumlem2  25024  selberglem1  25034  selberg2lem  25039  selberg3lem1  25046  selberg4  25050  pntrsumo1  25054  selberg34r  25060  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntlemb  25086  pntlemq  25090  pntlemr  25091  pntlemj  25092  pntlemo  25096  pnt2  25102  pnt  25103  padicabvcxp  25121  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ttgcontlem1  25565  brbtwn2  25585  colinearalglem1  25586  colinearalg  25590  axpaschlem  25620  axcontlem8  25651  numclwwlk1  26625  numclwwlk7  26641  smcnlem  26936  pjhthlem1  27634  kbmul  28198  kbass2  28360  2sqmod  28979  psgnfzto1st  29186  qqhval2lem  29353  qqhghm  29360  qqhrhm  29361  oddpwdc  29743  sgnmul  29931  plymulx0  29950  signsvtp  29986  signsvtn  29987  signsvfpn  29988  signsvfnn  29989  subfacval2  30423  subfaclim  30424  fwddifnp1  31442  knoppndvlem11  31683  knoppndvlem17  31689  bj-subcom  32331  bj-rdiv  32333  bj-bary1lem1  32338  itg2addnclem  32631  itg2addnclem2  32632  itgabsnc  32649  ftc1cnnclem  32653  areacirclem1  32670  areacirc  32675  geomcau  32725  bfplem1  32791  rrndstprj2  32800  rrnequiv  32804  irrapxlem5  36408  pellexlem2  36412  pellexlem6  36416  qirropth  36491  rmxyadd  36504  rmxm1  36517  rmxluc  36519  rmyluc2  36521  rmydbl  36523  jm2.24nn  36544  jm2.17a  36545  jm2.17b  36546  jm2.17c  36547  jm2.18  36573  jm2.19lem2  36575  jm2.22  36580  jm2.23  36581  areaquad  36821  imo72b2  37497  int-mulcomd  37501  int-rightdistd  37505  cvgdvgrat  37534  radcnvrat  37535  bccm1k  37563  binomcxplemwb  37569  binomcxplemnotnn0  37577  sineq0ALT  38195  mul13d  38432  divdiv3d  38516  mccllem  38664  coskpi2  38749  cosknegpi  38752  dvsinax  38801  dvasinbx  38810  dvcosax  38816  dvnxpaek  38832  dvnmul  38833  dvnprodlem2  38837  itgsinexplem1  38845  stoweidlem1  38894  stoweidlem11  38904  stoweidlem26  38919  stoweidlem32  38925  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem7  38973  stirlinglem10  38976  stirlinglem15  38981  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem1  38996  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem56  39055  fourierdlem66  39065  fourierdlem83  39082  fourierswlem  39123  fouriersw  39124  etransclem23  39150  etransclem24  39151  etransclem38  39165  etransclem46  39173  hoiprodp1  39478  hoidmvlelem2  39486  smfmullem1  39676  sigarac  39690  sigarls  39695  sigarid  39696  sigardiv  39699  sigarcol  39702  sigaradd  39704  cevathlem1  39705  fmtnoodd  39983  sqrtpwpw2p  39988  fmtnorec3  39998  fmtnoprmfac2lem1  40016  fmtnofac1  40020  pwdif  40039  lighneallem2  40061  lighneallem3  40062  proththd  40069  dfeven2  40100  av-numclwwlk1  41528  av-numclwwlk7  41545  altgsumbc  41923  altgsumbcALT  41924  blennnt2  42181  dignn0flhalflem2  42208  dignn0ehalf  42209  amgmwlem  42357