Theorem mulcomd 8354

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 8315	. 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 6088   CCcc 8184   x. cmul 8191

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

This theorem is used by:  mul31  8465  remulext2  8937  mulreim  8941  mulext2  8950  mulcanapd  8998  mulcanap2d  8999  divcanap1  9020  divrecap2  9028  div23ap  9030  divdivdivap  9052  divmuleqap  9056  divadddivap  9066  apmul2  9128  apdivmuld  9152  divcanap5rd  9157  dmdcanap2d  9160  mvllmulapd  9181  prodgt0  9191  lt2mul2div  9218  mulle0r  9283  subhalfhalf  9552  qapne  10055  irrmulap  10065  mul2lt0llt0  10179  mul2lt0lgt0  10180  mul2lt0pn  10182  modqvalr  10783  modqcyc  10817  mulp1mod1  10823  modqmul12d  10836  modqnegd  10837  modqmulmodr  10848  addmodlteq  10856  expaddzap  11041  binom2  11109  binom3  11115  bccmpl  11214  bcm1k  11220  bcn2  11224  bcpasc  11226  cvg1nlemcxze  11770  cvg1nlemcau  11772  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrexlemnm  11806  recvalap  11886  bdtrilem  12030  reccn2ap  12104  isummulc1  12219  fsummulc1  12241  trireciplem  12292  geolim  12303  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemfm  12321  cvgratz  12324  mertensabs  12329  eftlub  12482  sinadd  12528  cosadd  12529  sin2t  12541  nndivides  12589  dvds2ln  12616  even2n  12666  oddm1even  12667  m1exp1  12693  divalgmod  12719  bitsp1  12743  bitsinv1lem  12753  mulgcdr  12820  rplpwr  12829  lcmgcdlem  12880  divgcdcoprmex  12905  cncongr1  12906  nnmaxpwlemxy  12973  2sqpwodd  12981  eulerthlema  13037  eulerthlemth  13039  prmdiv  13042  prmdivdiv  13044  modprmn0modprm0  13064  coprimeprodsq  13065  pythagtriplem6  13078  pythagtriplem7  13079  pceulem  13102  pcadd  13148  prmpwdvds  13163  mul4sqlem  13201  4sqlem17  13215  evenennn  13342  mulgassr  14022  znunit  15103  dvmulxxbr  15961  dvmptcmulcn  15980  dvply1  16024  tangtx  16098  logdivlt  16157  cxpmul  16178  abscxp  16183  efnthr  16209  binom4  16252  pellexlem2  16263  wilthlem1  16265  mpodvdsmulf1o  16317  sgmppw  16319  perfect1  16331  lgsdirprm  16391  lgsdi  16394  lgsdirnn0  16404  lgsdinn0  16405  gausslemma2dlem1a  16415  gausslemma2dlem6  16424  lgsquadlem1  16434  lgsquadlem2  16435  lgsquadlem3  16436  lgsquad2  16440  2lgslem3a1  16454  2lgslem3b1  16455  2lgslem3c1  16456  2lgslem3d1  16457  2lgsoddprmlem2  16463  2sqlem3  16474  2sqlem4  16475  dichmul0orlem3  16993