Theorem mulcomd 11005

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   · cmul 10885

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

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

This theorem is referenced by:  mul31  11151  mul4r  11153  mulcand  11617  mulcan2d  11618  divcan1  11651  divrec2  11659  div23  11661  divdivdiv  11685  divmuleq  11689  divadddiv  11699  divcan5rd  11787  dmdcan2d  11790  mvllmuld  11816  rdiv  11819  subhalfhalf  12216  mul2lt0llt0  12843  mul2lt0lgt0  12844  prodge0ld  12847  xmulcom  13009  modvalr  13601  mulp1mod1  13641  modmul12d  13654  modnegd  13655  modmulmodr  13666  expaddz  13836  binom3  13948  expmulnbnd  13959  digit1  13961  bccmpl  14032  bcm1k  14038  bcn2  14042  bcpasc  14044  recval  15043  abs1m  15056  bhmafibid1cn  15184  bhmafibid2cn  15185  reccn2  15315  lo1mul2  15347  isummulc1  15484  fsummulc1  15506  incexclem  15557  incexc  15558  trireciplem  15583  pwdif  15589  geolim  15591  cvgrat  15604  mertens  15607  ntrivcvgmul  15623  fallfacfwd  15755  bpoly4  15778  fsumcube  15779  eftlub  15827  sinadd  15882  cosadd  15883  sin2t  15895  nndivides  15982  dvds2ln  16007  even2n  16060  oddm1even  16061  mod2eq1n2dvds  16065  m1exp1  16094  pwp1fsum  16109  divalgmod  16124  bitsp1  16147  bitsinv1lem  16157  sadadd2lem  16175  smumullem  16208  gcdmultiplez  16252  mulgcdr  16267  rplpwr  16276  lcmgcdlem  16320  divgcdcoprmex  16380  cncongr1  16381  eulerthlem2  16492  prmdiv  16495  prmdivdiv  16497  vfermltlALT  16512  modprmn0modprm0  16517  coprimeprodsq  16518  pythagtriplem6  16531  pythagtriplem7  16532  pceulem  16555  pcadd  16599  prmpwdvds  16614  mul4sqlem  16663  4sqlem17  16671  mulgassr  18750  odmodnn0  19157  odmulg  19172  odmulgeq  19173  odbezout  19174  odadd1  19458  ablfacrp2  19679  pgpfac1lem3  19689  zringlpirlem3  20695  znunit  20780  icopnfhmeo  24115  cphassr  24385  pjthlem1  24610  itgabs  25008  dvmulbr  25112  dvcmul  25117  dvcmulf  25118  dvmptcmul  25137  cmvth  25164  dvlipcn  25167  c1liplem1  25169  lhop1lem  25186  lhop2  25188  dvcvx  25193  dvfsumlem2  25200  ftc1lem4  25212  itgparts  25220  dvply1  25453  elqaalem3  25490  aalioulem4  25504  taylthlem2  25542  abelthlem6  25604  abelthlem7  25606  tangtx  25671  tanarg  25783  advlogexp  25819  mulcxp  25849  cxpmul  25852  abscxp  25856  dvcxp2  25903  cxpeq  25919  ang180lem1  25968  lawcoslem1  25974  lawcos  25975  heron  25997  dcubic1  26004  mcubic  26006  cubic2  26007  binom4  26009  dquart  26012  quart1lem  26014  quart1  26015  quartlem1  26016  dvatan  26094  leibpi  26101  log2cnv  26103  efrlim  26128  cxp2lim  26135  cxploglim  26136  zetacvg  26173  lgamgulmlem2  26188  lgamgulmlem3  26189  wilthlem1  26226  ftalem1  26231  ftalem5  26235  basellem3  26241  basellem5  26243  dvdsmulf1o  26352  sgmppw  26354  logfac2  26374  chpval2  26375  chpchtsum  26376  perfect1  26385  lgsdirprm  26488  lgsdi  26491  lgsdirnn0  26501  lgsdinn0  26502  gausslemma2dlem1a  26522  gausslemma2dlem6  26529  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  lgsquad2  26543  2lgslem3a1  26557  2lgslem3b1  26558  2lgslem3c1  26559  2lgslem3d1  26560  2lgsoddprmlem2  26566  2sqlem3  26577  2sqlem4  26578  2sqmod  26593  chebbnd1lem2  26627  chebbnd1lem3  26628  chtppilimlem2  26631  chto1lb  26635  rplogsumlem1  26641  dchrisumlem2  26647  dchrvmasum2lem  26653  dchrisum0flblem2  26666  dchrisum0lem2a  26674  mulogsumlem  26688  mulog2sumlem2  26692  selberglem1  26702  selberg2lem  26707  selberg3lem1  26714  selberg4  26718  pntrsumo1  26722  selberg34r  26728  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntlemb  26754  pntlemq  26758  pntlemr  26759  pntlemj  26760  pntlemo  26764  pnt2  26770  pnt  26771  padicabvcxp  26789  ostth2lem2  26791  ostth2lem3  26792  ostth2lem4  26793  ttgcontlem1  27261  brbtwn2  27282  colinearalglem1  27283  colinearalg  27287  axpaschlem  27317  axcontlem8  27348  numclwwlk1  28734  numclwwlk7  28764  smcnlem  29068  pjhthlem1  29762  kbmul  30326  kbass2  30488  psgnfzto1st  31381  ccfldextdgrr  31751  qqhval2lem  31940  qqhghm  31947  qqhrhm  31948  oddpwdc  32330  sgnmul  32518  plymulx0  32535  signsvtp  32571  signsvtn  32572  signsvfpn  32573  signsvfnn  32574  breprexplemc  32621  circlemethhgt  32632  logdivsqrle  32639  hgt750lemf  32642  hgt750lemb  32645  hgt750leme  32647  subfacval2  33158  subfaclim  33159  fwddifnp1  34476  knoppndvlem11  34711  knoppndvlem17  34717  bj-subcom  35488  bj-bary1lem1  35491  itg2addnclem  35837  itg2addnclem2  35838  itgabsnc  35855  ftc1cnnclem  35857  areacirclem1  35874  areacirc  35879  geomcau  35926  bfplem1  35989  rrndstprj2  35998  rrnequiv  36002  lcmineqlem1  40044  lcmineqlem5  40048  lcmineqlem8  40051  lcmineqlem11  40054  lcmineqlem18  40061  lcmineqlem21  40064  3lexlogpow5ineq2  40070  3lexlogpow2ineq1  40073  dvrelogpow2b  40083  aks4d1p1p7  40089  2np3bcnp1  40107  2ap1caineq  40108  3cubeslem2  40514  3cubeslem3l  40515  3cubeslem3r  40516  irrapxlem5  40655  pellexlem2  40659  pellexlem6  40663  qirropth  40737  rmxyadd  40750  rmxm1  40763  rmxluc  40765  rmyluc2  40767  rmydbl  40769  jm2.24nn  40788  jm2.17a  40789  jm2.17b  40790  jm2.17c  40791  jm2.18  40817  jm2.19lem2  40819  jm2.22  40824  jm2.23  40825  areaquad  41054  imo72b2  41790  int-mulcomd  41794  int-rightdistd  41798  cvgdvgrat  41938  radcnvrat  41939  bccm1k  41967  binomcxplemwb  41973  binomcxplemnotnn0  41981  sineq0ALT  42564  mul13d  42825  divdiv3d  42905  mccllem  43145  coskpi2  43414  cosknegpi  43417  dvsinax  43461  dvasinbx  43468  dvcosax  43474  dvnxpaek  43490  dvnmul  43491  dvnprodlem2  43495  itgsinexplem1  43502  stoweidlem1  43549  stoweidlem11  43559  stoweidlem26  43574  stoweidlem32  43580  wallispilem4  43616  wallispi2lem1  43619  wallispi2lem2  43620  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem7  43628  stirlinglem10  43631  stirlinglem15  43636  dirkertrigeqlem1  43646  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem1  43651  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem56  43710  fourierdlem66  43720  fourierdlem83  43737  fourierswlem  43778  fouriersw  43779  etransclem23  43805  etransclem24  43806  etransclem38  43820  etransclem46  43828  hoiprodp1  44133  hoidmvlelem2  44141  smfmullem1  44336  sigarac  44379  sigarls  44384  sigarid  44385  sigardiv  44388  sigarcol  44391  sigaradd  44393  cevathlem1  44394  sqrtnegnre  44810  fmtnoodd  44996  sqrtpwpw2p  45001  fmtnorec3  45011  fmtnoprmfac2lem1  45029  fmtnofac1  45033  lighneallem2  45069  lighneallem3  45070  proththd  45077  requad01  45084  dfeven2  45112  fppr2odd  45194  fpprwppr  45202  altgsumbc  45699  altgsumbcALT  45700  blennnt2  45946  dignn0flhalflem2  45973  dignn0ehalf  45974  itcovalt2lem2lem2  46031  affinecomb2  46060  rrx2linest  46099  itscnhlc0yqe  46116  itsclc0yqsollem1  46119  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123  itsclc0xyqsolr  46126  itsclquadb  46133  2itscplem3  46137  itscnhlinecirc02plem1  46139  itscnhlinecirc02plem2  46140  inlinecirc02p  46144  amgmwlem  46517