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  10777  modqcyc  10811  mulp1mod1  10817  modqmul12d  10830  modqnegd  10831  modqmulmodr  10842  addmodlteq  10850  expaddzap  11035  binom2  11103  binom3  11109  bccmpl  11208  bcm1k  11214  bcn2  11218  bcpasc  11220  cvg1nlemcxze  11764  cvg1nlemcau  11766  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrexlemnm  11800  recvalap  11880  bdtrilem  12024  reccn2ap  12098  isummulc1  12213  fsummulc1  12235  trireciplem  12286  geolim  12297  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemfm  12315  cvgratz  12318  mertensabs  12323  eftlub  12476  sinadd  12522  cosadd  12523  sin2t  12535  nndivides  12583  dvds2ln  12610  even2n  12660  oddm1even  12661  m1exp1  12687  divalgmod  12713  bitsp1  12737  bitsinv1lem  12747  mulgcdr  12814  rplpwr  12823  lcmgcdlem  12874  divgcdcoprmex  12899  cncongr1  12900  nnmaxpwlemxy  12967  2sqpwodd  12975  eulerthlema  13031  eulerthlemth  13033  prmdiv  13036  prmdivdiv  13038  modprmn0modprm0  13058  coprimeprodsq  13059  pythagtriplem6  13072  pythagtriplem7  13073  pceulem  13096  pcadd  13142  prmpwdvds  13157  mul4sqlem  13195  4sqlem17  13209  evenennn  13336  mulgassr  14016  znunit  15085  dvmulxxbr  15902  dvmptcmulcn  15921  dvply1  15965  tangtx  16039  logdivlt  16098  cxpmul  16119  abscxp  16124  efnthr  16150  binom4  16193  pellexlem2  16204  wilthlem1  16206  mpodvdsmulf1o  16258  sgmppw  16260  perfect1  16272  lgsdirprm  16332  lgsdi  16335  lgsdirnn0  16345  lgsdinn0  16346  gausslemma2dlem1a  16356  gausslemma2dlem6  16365  lgsquadlem1  16375  lgsquadlem2  16376  lgsquadlem3  16377  lgsquad2  16381  2lgslem3a1  16395  2lgslem3b1  16396  2lgslem3c1  16397  2lgslem3d1  16398  2lgsoddprmlem2  16404  2sqlem3  16415  2sqlem4  16416  dichmul0orlem3  16934