Theorem mulcomd 8348

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 8309	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A x. B ) = ( B x. A ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   x. cmul 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcom 8281

This theorem is used by:  mul31  8459  remulext2  8931  mulreim  8935  mulext2  8944  mulcanapd  8992  mulcanap2d  8993  divcanap1  9014  divrecap2  9022  div23ap  9024  divdivdivap  9046  divmuleqap  9050  divadddivap  9060  apmul2  9122  apdivmuld  9146  divcanap5rd  9151  dmdcanap2d  9154  mvllmulapd  9175  prodgt0  9185  lt2mul2div  9212  mulle0r  9277  subhalfhalf  9545  qapne  10049  irrmulap  10059  mul2lt0llt0  10173  mul2lt0lgt0  10174  mul2lt0pn  10176  modqvalr  10776  modqcyc  10810  mulp1mod1  10816  modqmul12d  10829  modqnegd  10830  modqmulmodr  10841  addmodlteq  10849  expaddzap  11034  binom2  11102  binom3  11108  bccmpl  11207  bcm1k  11213  bcn2  11217  bcpasc  11219  cvg1nlemcxze  11763  cvg1nlemcau  11765  resqrexlemcalc1  11795  resqrexlemcalc2  11796  resqrexlemnm  11799  recvalap  11879  bdtrilem  12023  reccn2ap  12097  isummulc1  12212  fsummulc1  12234  trireciplem  12285  geolim  12296  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  cvgratnnlemfm  12314  cvgratz  12317  mertensabs  12322  eftlub  12475  sinadd  12521  cosadd  12522  sin2t  12534  nndivides  12582  dvds2ln  12609  even2n  12659  oddm1even  12660  m1exp1  12686  divalgmod  12712  bitsp1  12736  bitsinv1lem  12746  mulgcdr  12813  rplpwr  12822  lcmgcdlem  12873  divgcdcoprmex  12898  cncongr1  12899  nnmaxpwlemxy  12966  2sqpwodd  12974  eulerthlema  13030  eulerthlemth  13032  prmdiv  13035  prmdivdiv  13037  modprmn0modprm0  13057  coprimeprodsq  13058  pythagtriplem6  13071  pythagtriplem7  13072  pceulem  13095  pcadd  13141  prmpwdvds  13156  mul4sqlem  13194  4sqlem17  13208  evenennn  13335  mulgassr  14014  znunit  15045  dvmulxxbr  15855  dvmptcmulcn  15874  dvply1  15918  tangtx  15992  logdivlt  16049  cxpmul  16070  abscxp  16073  binom4  16141  pellexlem2  16152  wilthlem1  16154  mpodvdsmulf1o  16206  sgmppw  16208  perfect1  16220  lgsdirprm  16275  lgsdi  16278  lgsdirnn0  16288  lgsdinn0  16289  gausslemma2dlem1a  16299  gausslemma2dlem6  16308  lgsquadlem1  16318  lgsquadlem2  16319  lgsquadlem3  16320  lgsquad2  16324  2lgslem3a1  16338  2lgslem3b1  16339  2lgslem3c1  16340  2lgslem3d1  16341  2lgsoddprmlem2  16347  2sqlem3  16358  2sqlem4  16359  dichmul0orlem3  16877