Theorem mulcomd 10061

Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	|- ( ph -> A e. CC )
addcld.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
mulcomd	|- ( ph -> ( A x. B ) = ( B x. A ) )

Proof of Theorem mulcomd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		mulcom 10022	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ( A x. B ) = ( B x. A ) )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   x. cmul 9941

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mul31  10204  subdir2d  10488  mulcand  10660  mulcan2d  10661  divcan1  10694  divrec2  10702  div23  10704  divdivdiv  10726  divmuleq  10730  divadddiv  10740  divcan5rd  10828  dmdcan2d  10831  mvllmuld  10857  subhalfhalf  11266  mul2lt0llt0  11934  mul2lt0lgt0  11935  xmulcom  12096  modvalr  12671  mulp1mod1  12711  modmul12d  12724  modnegd  12725  modmulmodr  12736  expaddz  12904  binom3  12985  expmulnbnd  12996  digit1  12998  bccmpl  13096  bcm1k  13102  bcn2  13106  bcpasc  13108  recval  14062  abs1m  14075  reccn2  14327  lo1mul2  14359  isummulc1  14494  fsummulc1  14517  incexclem  14568  incexc  14569  trireciplem  14594  geolim  14601  cvgrat  14615  mertens  14618  ntrivcvgmul  14634  fallfacfwd  14767  bpoly4  14790  fsumcube  14791  eftlub  14839  sinadd  14894  cosadd  14895  sin2t  14907  nndivides  14990  dvds2ln  15014  even2n  15066  oddm1even  15067  mod2eq1n2dvds  15071  m1exp1  15093  pwp1fsum  15114  divalgmod  15129  divalgmodOLD  15130  bitsp1  15153  bitsinv1lem  15163  sadadd2lem  15181  smumullem  15214  mulgcdr  15267  rplpwr  15276  lcmgcdlem  15319  divgcdcoprmex  15380  cncongr1  15381  eulerthlem2  15487  prmdiv  15490  prmdivdiv  15492  vfermltlALT  15507  modprmn0modprm0  15512  coprimeprodsq  15513  pythagtriplem6  15526  pythagtriplem7  15527  pceulem  15550  pcadd  15593  prmpwdvds  15608  mul4sqlem  15657  4sqlem17  15665  mulgassr  17580  odmodnn0  17959  odmulg  17973  odmulgeq  17974  odbezout  17975  odadd1  18251  ablfacrp2  18466  pgpfac1lem3  18476  zringlpirlem3  19834  znunit  19912  icopnfhmeo  22742  cphassr  23012  pjthlem1  23208  itgabs  23601  dvmulbr  23702  dvcmul  23707  dvcmulf  23708  dvmptcmul  23727  cmvth  23754  dvlipcn  23757  c1liplem1  23759  lhop1lem  23776  lhop2  23778  dvcvx  23783  dvfsumlem2  23790  ftc1lem4  23802  itgparts  23810  dvply1  24039  elqaalem3  24076  aalioulem4  24090  taylthlem2  24128  abelthlem6  24190  abelthlem7  24192  tangtx  24257  tanarg  24365  advlogexp  24401  mulcxp  24431  cxpmul  24434  abscxp  24438  dvcxp2  24482  cxpeq  24498  ang180lem1  24539  lawcoslem1  24545  lawcos  24546  heron  24565  dcubic1  24572  mcubic  24574  cubic2  24575  binom4  24577  dquart  24580  quart1lem  24582  quart1  24583  quartlem1  24584  dvatan  24662  leibpi  24669  log2cnv  24671  efrlim  24696  cxp2lim  24703  cxploglim  24704  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem3  24757  wilthlem1  24794  ftalem1  24799  ftalem5  24803  basellem3  24809  basellem5  24811  dvdsmulf1o  24920  sgmppw  24922  logfac2  24942  chpval2  24943  chpchtsum  24944  perfect1  24953  lgsdirprm  25056  lgsdi  25059  lgsdirnn0  25069  lgsdinn0  25070  gausslemma2dlem1a  25090  gausslemma2dlem6  25097  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2  25111  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  2lgsoddprmlem2  25134  2sqlem3  25145  2sqlem4  25146  chebbnd1lem2  25159  chebbnd1lem3  25160  chtppilimlem2  25163  chto1lb  25167  rplogsumlem1  25173  dchrisumlem2  25179  dchrvmasum2lem  25185  dchrisum0flblem2  25198  dchrisum0lem2a  25206  mulogsumlem  25220  mulog2sumlem2  25224  selberglem1  25234  selberg2lem  25239  selberg3lem1  25246  selberg4  25250  pntrsumo1  25254  selberg34r  25260  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntlemb  25286  pntlemq  25290  pntlemr  25291  pntlemj  25292  pntlemo  25296  pnt2  25302  pnt  25303  padicabvcxp  25321  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ttgcontlem1  25765  brbtwn2  25785  colinearalglem1  25786  colinearalg  25790  axpaschlem  25820  axcontlem8  25851  numclwwlk1  27231  numclwwlk7  27249  smcnlem  27552  pjhthlem1  28250  kbmul  28814  kbass2  28976  2sqmod  29648  psgnfzto1st  29855  qqhval2lem  30025  qqhghm  30032  qqhrhm  30033  oddpwdc  30416  sgnmul  30604  plymulx0  30624  signsvtp  30660  signsvtn  30661  signsvfpn  30662  signsvfnn  30663  breprexplemc  30710  circlemethhgt  30721  logdivsqrle  30728  hgt750lemf  30731  hgt750lemb  30734  hgt750leme  30736  subfacval2  31169  subfaclim  31170  fwddifnp1  32272  knoppndvlem11  32513  knoppndvlem17  32519  bj-subcom  33154  bj-rdiv  33156  bj-bary1lem1  33161  itg2addnclem  33461  itg2addnclem2  33462  itgabsnc  33479  ftc1cnnclem  33483  areacirclem1  33500  areacirc  33505  geomcau  33555  bfplem1  33621  rrndstprj2  33630  rrnequiv  33634  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  qirropth  37473  rmxyadd  37486  rmxm1  37499  rmxluc  37501  rmyluc2  37503  rmydbl  37505  jm2.24nn  37526  jm2.17a  37527  jm2.17b  37528  jm2.17c  37529  jm2.18  37555  jm2.19lem2  37557  jm2.22  37562  jm2.23  37563  areaquad  37802  imo72b2  38475  int-mulcomd  38479  int-rightdistd  38483  cvgdvgrat  38512  radcnvrat  38513  bccm1k  38541  binomcxplemwb  38547  binomcxplemnotnn0  38555  sineq0ALT  39173  mul13d  39491  divdiv3d  39575  mccllem  39829  coskpi2  40077  cosknegpi  40080  dvsinax  40127  dvasinbx  40135  dvcosax  40141  dvnxpaek  40157  dvnmul  40158  dvnprodlem2  40162  itgsinexplem1  40169  stoweidlem1  40218  stoweidlem11  40228  stoweidlem26  40243  stoweidlem32  40249  wallispilem4  40285  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem7  40297  stirlinglem10  40300  stirlinglem15  40305  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem1  40320  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem56  40379  fourierdlem66  40389  fourierdlem83  40406  fourierswlem  40447  fouriersw  40448  etransclem23  40474  etransclem24  40475  etransclem38  40489  etransclem46  40497  hoiprodp1  40802  hoidmvlelem2  40810  smfmullem1  40998  sigarac  41041  sigarls  41046  sigarid  41047  sigardiv  41050  sigarcol  41053  sigaradd  41055  cevathlem1  41056  fmtnoodd  41445  sqrtpwpw2p  41450  fmtnorec3  41460  fmtnoprmfac2lem1  41478  fmtnofac1  41482  pwdif  41501  lighneallem2  41523  lighneallem3  41524  proththd  41531  dfeven2  41562  altgsumbc  42130  altgsumbcALT  42131  blennnt2  42383  dignn0flhalflem2  42410  dignn0ehalf  42411  amgmwlem  42548