Theorem mulcomd 10740

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7170  ℂcc 10613   · cmul 10620

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

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  mul31  10885  mul4r  10887  mulcand  11351  mulcan2d  11352  divcan1  11385  divrec2  11393  div23  11395  divdivdiv  11419  divmuleq  11423  divadddiv  11433  divcan5rd  11521  dmdcan2d  11524  mvllmuld  11550  rdiv  11553  subhalfhalf  11950  mul2lt0llt0  12576  mul2lt0lgt0  12577  prodge0ld  12580  xmulcom  12742  modvalr  13331  mulp1mod1  13371  modmul12d  13384  modnegd  13385  modmulmodr  13396  expaddz  13565  binom3  13677  expmulnbnd  13688  digit1  13690  bccmpl  13761  bcm1k  13767  bcn2  13771  bcpasc  13773  recval  14772  abs1m  14785  bhmafibid1cn  14913  bhmafibid2cn  14914  reccn2  15044  lo1mul2  15076  isummulc1  15211  fsummulc1  15233  incexclem  15284  incexc  15285  trireciplem  15310  pwdif  15316  geolim  15318  cvgrat  15331  mertens  15334  ntrivcvgmul  15350  fallfacfwd  15482  bpoly4  15505  fsumcube  15506  eftlub  15554  sinadd  15609  cosadd  15610  sin2t  15622  nndivides  15709  dvds2ln  15734  even2n  15787  oddm1even  15788  mod2eq1n2dvds  15792  m1exp1  15821  pwp1fsum  15836  divalgmod  15851  bitsp1  15874  bitsinv1lem  15884  sadadd2lem  15902  smumullem  15935  gcdmultiplez  15979  mulgcdr  15994  rplpwr  16003  lcmgcdlem  16047  divgcdcoprmex  16107  cncongr1  16108  eulerthlem2  16219  prmdiv  16222  prmdivdiv  16224  vfermltlALT  16239  modprmn0modprm0  16244  coprimeprodsq  16245  pythagtriplem6  16258  pythagtriplem7  16259  pceulem  16282  pcadd  16325  prmpwdvds  16340  mul4sqlem  16389  4sqlem17  16397  mulgassr  18383  odmodnn0  18786  odmulg  18801  odmulgeq  18802  odbezout  18803  odadd1  19087  ablfacrp2  19308  pgpfac1lem3  19318  zringlpirlem3  20305  znunit  20382  icopnfhmeo  23695  cphassr  23964  pjthlem1  24189  itgabs  24587  dvmulbr  24691  dvcmul  24696  dvcmulf  24697  dvmptcmul  24716  cmvth  24743  dvlipcn  24746  c1liplem1  24748  lhop1lem  24765  lhop2  24767  dvcvx  24772  dvfsumlem2  24779  ftc1lem4  24791  itgparts  24799  dvply1  25032  elqaalem3  25069  aalioulem4  25083  taylthlem2  25121  abelthlem6  25183  abelthlem7  25185  tangtx  25250  tanarg  25362  advlogexp  25398  mulcxp  25428  cxpmul  25431  abscxp  25435  dvcxp2  25482  cxpeq  25498  ang180lem1  25547  lawcoslem1  25553  lawcos  25554  heron  25576  dcubic1  25583  mcubic  25585  cubic2  25586  binom4  25588  dquart  25591  quart1lem  25593  quart1  25594  quartlem1  25595  dvatan  25673  leibpi  25680  log2cnv  25682  efrlim  25707  cxp2lim  25714  cxploglim  25715  zetacvg  25752  lgamgulmlem2  25767  lgamgulmlem3  25768  wilthlem1  25805  ftalem1  25810  ftalem5  25814  basellem3  25820  basellem5  25822  dvdsmulf1o  25931  sgmppw  25933  logfac2  25953  chpval2  25954  chpchtsum  25955  perfect1  25964  lgsdirprm  26067  lgsdi  26070  lgsdirnn0  26080  lgsdinn0  26081  gausslemma2dlem1a  26101  gausslemma2dlem6  26108  lgsquadlem1  26116  lgsquadlem2  26117  lgsquadlem3  26118  lgsquad2  26122  2lgslem3a1  26136  2lgslem3b1  26137  2lgslem3c1  26138  2lgslem3d1  26139  2lgsoddprmlem2  26145  2sqlem3  26156  2sqlem4  26157  2sqmod  26172  chebbnd1lem2  26206  chebbnd1lem3  26207  chtppilimlem2  26210  chto1lb  26214  rplogsumlem1  26220  dchrisumlem2  26226  dchrvmasum2lem  26232  dchrisum0flblem2  26245  dchrisum0lem2a  26253  mulogsumlem  26267  mulog2sumlem2  26271  selberglem1  26281  selberg2lem  26286  selberg3lem1  26293  selberg4  26297  pntrsumo1  26301  selberg34r  26307  pntrlog2bndlem3  26315  pntrlog2bndlem4  26316  pntlemb  26333  pntlemq  26337  pntlemr  26338  pntlemj  26339  pntlemo  26343  pnt2  26349  pnt  26350  padicabvcxp  26368  ostth2lem2  26370  ostth2lem3  26371  ostth2lem4  26372  ttgcontlem1  26831  brbtwn2  26851  colinearalglem1  26852  colinearalg  26856  axpaschlem  26886  axcontlem8  26917  numclwwlk1  28298  numclwwlk7  28328  smcnlem  28632  pjhthlem1  29326  kbmul  29890  kbass2  30052  psgnfzto1st  30949  ccfldextdgrr  31314  qqhval2lem  31501  qqhghm  31508  qqhrhm  31509  oddpwdc  31891  sgnmul  32079  plymulx0  32096  signsvtp  32132  signsvtn  32133  signsvfpn  32134  signsvfnn  32135  breprexplemc  32182  circlemethhgt  32193  logdivsqrle  32200  hgt750lemf  32203  hgt750lemb  32206  hgt750leme  32208  subfacval2  32720  subfaclim  32721  fwddifnp1  34105  knoppndvlem11  34340  knoppndvlem17  34346  bj-subcom  35099  bj-bary1lem1  35102  itg2addnclem  35451  itg2addnclem2  35452  itgabsnc  35469  ftc1cnnclem  35471  areacirclem1  35488  areacirc  35493  geomcau  35540  bfplem1  35603  rrndstprj2  35612  rrnequiv  35616  lcmineqlem1  39657  lcmineqlem5  39661  lcmineqlem8  39664  lcmineqlem11  39667  lcmineqlem18  39674  lcmineqlem21  39677  3lexlogpow5ineq2  39683  3lexlogpow2ineq1  39686  dvrelogpow2b  39695  aks4d1p1p7  39701  2np3bcnp1  39706  2ap1caineq  39707  3cubeslem2  40079  3cubeslem3l  40080  3cubeslem3r  40081  irrapxlem5  40220  pellexlem2  40224  pellexlem6  40228  qirropth  40302  rmxyadd  40315  rmxm1  40328  rmxluc  40330  rmyluc2  40332  rmydbl  40334  jm2.24nn  40353  jm2.17a  40354  jm2.17b  40355  jm2.17c  40356  jm2.18  40382  jm2.19lem2  40384  jm2.22  40389  jm2.23  40390  areaquad  40619  imo72b2  41330  int-mulcomd  41334  int-rightdistd  41338  cvgdvgrat  41469  radcnvrat  41470  bccm1k  41498  binomcxplemwb  41504  binomcxplemnotnn0  41512  sineq0ALT  42095  mul13d  42355  divdiv3d  42436  mccllem  42680  coskpi2  42949  cosknegpi  42952  dvsinax  42996  dvasinbx  43003  dvcosax  43009  dvnxpaek  43025  dvnmul  43026  dvnprodlem2  43030  itgsinexplem1  43037  stoweidlem1  43084  stoweidlem11  43094  stoweidlem26  43109  stoweidlem32  43115  wallispilem4  43151  wallispi2lem1  43154  wallispi2lem2  43155  stirlinglem3  43159  stirlinglem4  43160  stirlinglem5  43161  stirlinglem7  43163  stirlinglem10  43166  stirlinglem15  43171  dirkertrigeqlem1  43181  dirkertrigeqlem2  43182  dirkertrigeqlem3  43183  dirkertrigeq  43184  dirkercncflem1  43186  fourierdlem16  43206  fourierdlem21  43211  fourierdlem22  43212  fourierdlem56  43245  fourierdlem66  43255  fourierdlem83  43272  fourierswlem  43313  fouriersw  43314  etransclem23  43340  etransclem24  43341  etransclem38  43355  etransclem46  43363  hoiprodp1  43668  hoidmvlelem2  43676  smfmullem1  43864  sigarac  43907  sigarls  43912  sigarid  43913  sigardiv  43916  sigarcol  43919  sigaradd  43921  cevathlem1  43922  sqrtnegnre  44333  fmtnoodd  44519  sqrtpwpw2p  44524  fmtnorec3  44534  fmtnoprmfac2lem1  44552  fmtnofac1  44556  lighneallem2  44592  lighneallem3  44593  proththd  44600  requad01  44607  dfeven2  44635  fppr2odd  44717  fpprwppr  44725  altgsumbc  45222  altgsumbcALT  45223  blennnt2  45469  dignn0flhalflem2  45496  dignn0ehalf  45497  itcovalt2lem2lem2  45554  affinecomb2  45583  rrx2linest  45622  itscnhlc0yqe  45639  itsclc0yqsollem1  45642  itscnhlc0xyqsol  45645  itschlc0xyqsol1  45646  itsclc0xyqsolr  45649  itsclquadb  45656  2itscplem3  45660  itscnhlinecirc02plem1  45662  itscnhlinecirc02plem2  45663  inlinecirc02p  45667  amgmwlem  45959