Theorem mulcomd 10662

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   · cmul 10542

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mul31  10807  mul4r  10809  mulcand  11273  mulcan2d  11274  divcan1  11307  divrec2  11315  div23  11317  divdivdiv  11341  divmuleq  11345  divadddiv  11355  divcan5rd  11443  dmdcan2d  11446  mvllmuld  11472  rdiv  11475  subhalfhalf  11872  mul2lt0llt0  12494  mul2lt0lgt0  12495  prodge0ld  12498  xmulcom  12660  modvalr  13241  mulp1mod1  13281  modmul12d  13294  modnegd  13295  modmulmodr  13306  expaddz  13474  binom3  13586  expmulnbnd  13597  digit1  13599  bccmpl  13670  bcm1k  13676  bcn2  13680  bcpasc  13682  recval  14682  abs1m  14695  bhmafibid1cn  14823  bhmafibid2cn  14824  reccn2  14953  lo1mul2  14985  isummulc1  15118  fsummulc1  15140  incexclem  15191  incexc  15192  trireciplem  15217  pwdif  15223  geolim  15226  cvgrat  15239  mertens  15242  ntrivcvgmul  15258  fallfacfwd  15390  bpoly4  15413  fsumcube  15414  eftlub  15462  sinadd  15517  cosadd  15518  sin2t  15530  nndivides  15617  dvds2ln  15642  even2n  15691  oddm1even  15692  mod2eq1n2dvds  15696  m1exp1  15727  pwp1fsum  15742  divalgmod  15757  bitsp1  15780  bitsinv1lem  15790  sadadd2lem  15808  smumullem  15841  gcdmultiplez  15883  mulgcdr  15898  rplpwr  15907  lcmgcdlem  15950  divgcdcoprmex  16010  cncongr1  16011  eulerthlem2  16119  prmdiv  16122  prmdivdiv  16124  vfermltlALT  16139  modprmn0modprm0  16144  coprimeprodsq  16145  pythagtriplem6  16158  pythagtriplem7  16159  pceulem  16182  pcadd  16225  prmpwdvds  16240  mul4sqlem  16289  4sqlem17  16297  mulgassr  18265  odmodnn0  18668  odmulg  18683  odmulgeq  18684  odbezout  18685  odadd1  18968  ablfacrp2  19189  pgpfac1lem3  19199  zringlpirlem3  20633  znunit  20710  icopnfhmeo  23547  cphassr  23816  pjthlem1  24040  itgabs  24435  dvmulbr  24536  dvcmul  24541  dvcmulf  24542  dvmptcmul  24561  cmvth  24588  dvlipcn  24591  c1liplem1  24593  lhop1lem  24610  lhop2  24612  dvcvx  24617  dvfsumlem2  24624  ftc1lem4  24636  itgparts  24644  dvply1  24873  elqaalem3  24910  aalioulem4  24924  taylthlem2  24962  abelthlem6  25024  abelthlem7  25026  tangtx  25091  tanarg  25202  advlogexp  25238  mulcxp  25268  cxpmul  25271  abscxp  25275  dvcxp2  25322  cxpeq  25338  ang180lem1  25387  lawcoslem1  25393  lawcos  25394  heron  25416  dcubic1  25423  mcubic  25425  cubic2  25426  binom4  25428  dquart  25431  quart1lem  25433  quart1  25434  quartlem1  25435  dvatan  25513  leibpi  25520  log2cnv  25522  efrlim  25547  cxp2lim  25554  cxploglim  25555  zetacvg  25592  lgamgulmlem2  25607  lgamgulmlem3  25608  wilthlem1  25645  ftalem1  25650  ftalem5  25654  basellem3  25660  basellem5  25662  dvdsmulf1o  25771  sgmppw  25773  logfac2  25793  chpval2  25794  chpchtsum  25795  perfect1  25804  lgsdirprm  25907  lgsdi  25910  lgsdirnn0  25920  lgsdinn0  25921  gausslemma2dlem1a  25941  gausslemma2dlem6  25948  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  lgsquad2  25962  2lgslem3a1  25976  2lgslem3b1  25977  2lgslem3c1  25978  2lgslem3d1  25979  2lgsoddprmlem2  25985  2sqlem3  25996  2sqlem4  25997  2sqmod  26012  chebbnd1lem2  26046  chebbnd1lem3  26047  chtppilimlem2  26050  chto1lb  26054  rplogsumlem1  26060  dchrisumlem2  26066  dchrvmasum2lem  26072  dchrisum0flblem2  26085  dchrisum0lem2a  26093  mulogsumlem  26107  mulog2sumlem2  26111  selberglem1  26121  selberg2lem  26126  selberg3lem1  26133  selberg4  26137  pntrsumo1  26141  selberg34r  26147  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntlemb  26173  pntlemq  26177  pntlemr  26178  pntlemj  26179  pntlemo  26183  pnt2  26189  pnt  26190  padicabvcxp  26208  ostth2lem2  26210  ostth2lem3  26211  ostth2lem4  26212  ttgcontlem1  26671  brbtwn2  26691  colinearalglem1  26692  colinearalg  26696  axpaschlem  26726  axcontlem8  26757  numclwwlk1  28140  numclwwlk7  28170  smcnlem  28474  pjhthlem1  29168  kbmul  29732  kbass2  29894  psgnfzto1st  30747  ccfldextdgrr  31057  qqhval2lem  31222  qqhghm  31229  qqhrhm  31230  oddpwdc  31612  sgnmul  31800  plymulx0  31817  signsvtp  31853  signsvtn  31854  signsvfpn  31855  signsvfnn  31856  breprexplemc  31903  circlemethhgt  31914  logdivsqrle  31921  hgt750lemf  31924  hgt750lemb  31927  hgt750leme  31929  subfacval2  32434  subfaclim  32435  fwddifnp1  33626  knoppndvlem11  33861  knoppndvlem17  33867  bj-subcom  34592  bj-bary1lem1  34595  itg2addnclem  34958  itg2addnclem2  34959  itgabsnc  34976  ftc1cnnclem  34980  areacirclem1  34997  areacirc  35002  geomcau  35049  bfplem1  35115  rrndstprj2  35124  rrnequiv  35128  3cubeslem2  39331  3cubeslem3l  39332  3cubeslem3r  39333  irrapxlem5  39472  pellexlem2  39476  pellexlem6  39480  qirropth  39554  rmxyadd  39567  rmxm1  39580  rmxluc  39582  rmyluc2  39584  rmydbl  39586  jm2.24nn  39605  jm2.17a  39606  jm2.17b  39607  jm2.17c  39608  jm2.18  39634  jm2.19lem2  39636  jm2.22  39641  jm2.23  39642  areaquad  39872  imo72b2  40574  int-mulcomd  40578  int-rightdistd  40582  cvgdvgrat  40694  radcnvrat  40695  bccm1k  40723  binomcxplemwb  40729  binomcxplemnotnn0  40737  sineq0ALT  41320  mul13d  41594  divdiv3d  41676  mccllem  41927  coskpi2  42196  cosknegpi  42199  dvsinax  42246  dvasinbx  42254  dvcosax  42260  dvnxpaek  42276  dvnmul  42277  dvnprodlem2  42281  itgsinexplem1  42288  stoweidlem1  42335  stoweidlem11  42345  stoweidlem26  42360  stoweidlem32  42366  wallispilem4  42402  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem3  42410  stirlinglem4  42411  stirlinglem5  42412  stirlinglem7  42414  stirlinglem10  42417  stirlinglem15  42422  dirkertrigeqlem1  42432  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkercncflem1  42437  fourierdlem16  42457  fourierdlem21  42462  fourierdlem22  42463  fourierdlem56  42496  fourierdlem66  42506  fourierdlem83  42523  fourierswlem  42564  fouriersw  42565  etransclem23  42591  etransclem24  42592  etransclem38  42606  etransclem46  42614  hoiprodp1  42919  hoidmvlelem2  42927  smfmullem1  43115  sigarac  43158  sigarls  43163  sigarid  43164  sigardiv  43167  sigarcol  43170  sigaradd  43172  cevathlem1  43173  sqrtnegnre  43556  fmtnoodd  43744  sqrtpwpw2p  43749  fmtnorec3  43759  fmtnoprmfac2lem1  43777  fmtnofac1  43781  lighneallem2  43820  lighneallem3  43821  proththd  43828  requad01  43835  dfeven2  43863  fppr2odd  43945  fpprwppr  43953  altgsumbc  44449  altgsumbcALT  44450  blennnt2  44698  dignn0flhalflem2  44725  dignn0ehalf  44726  affinecomb2  44739  rrx2linest  44778  itscnhlc0yqe  44795  itsclc0yqsollem1  44798  itscnhlc0xyqsol  44801  itschlc0xyqsol1  44802  itsclc0xyqsolr  44805  itsclquadb  44812  2itscplem3  44816  itscnhlinecirc02plem1  44818  itscnhlinecirc02plem2  44819  inlinecirc02p  44823  amgmwlem  44952