Theorem mulcomd 8107

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2177  (class class class)co 5954   CCcc 7936   x. cmul 7943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcom 8039

This theorem is referenced by:  mul31  8216  remulext2  8686  mulreim  8690  mulext2  8699  mulcanapd  8747  mulcanap2d  8748  divcanap1  8767  divrecap2  8775  div23ap  8777  divdivdivap  8799  divmuleqap  8803  divadddivap  8813  apmul2  8875  apdivmuld  8899  divcanap5rd  8904  dmdcanap2d  8907  mvllmulapd  8928  prodgt0  8938  lt2mul2div  8965  mulle0r  9030  subhalfhalf  9285  qapne  9773  irrmulap  9782  mul2lt0llt0  9896  mul2lt0lgt0  9897  mul2lt0pn  9899  modqvalr  10483  modqcyc  10517  mulp1mod1  10523  modqmul12d  10536  modqnegd  10537  modqmulmodr  10548  addmodlteq  10556  expaddzap  10741  binom2  10809  binom3  10815  bccmpl  10912  bcm1k  10918  bcn2  10922  bcpasc  10924  cvg1nlemcxze  11343  cvg1nlemcau  11345  resqrexlemcalc1  11375  resqrexlemcalc2  11376  resqrexlemnm  11379  recvalap  11458  bdtrilem  11600  reccn2ap  11674  isummulc1  11788  fsummulc1  11810  trireciplem  11861  geolim  11872  cvgratnnlemnexp  11885  cvgratnnlemmn  11886  cvgratnnlemfm  11890  cvgratz  11893  mertensabs  11898  eftlub  12051  sinadd  12097  cosadd  12098  sin2t  12110  nndivides  12158  dvds2ln  12185  even2n  12235  oddm1even  12236  m1exp1  12262  divalgmod  12288  bitsp1  12312  bitsinv1lem  12322  mulgcdr  12389  rplpwr  12398  lcmgcdlem  12449  divgcdcoprmex  12474  cncongr1  12475  oddpwdclemxy  12541  2sqpwodd  12548  eulerthlema  12602  eulerthlemth  12604  prmdiv  12607  prmdivdiv  12609  modprmn0modprm0  12629  coprimeprodsq  12630  pythagtriplem6  12643  pythagtriplem7  12644  pceulem  12667  pcadd  12713  prmpwdvds  12728  mul4sqlem  12766  4sqlem17  12780  evenennn  12814  mulgassr  13546  znunit  14471  dvmulxxbr  15224  dvmptcmulcn  15243  dvply1  15287  tangtx  15360  cxpmul  15434  abscxp  15437  binom4  15501  wilthlem1  15502  mpodvdsmulf1o  15512  sgmppw  15514  perfect1  15520  lgsdirprm  15561  lgsdi  15564  lgsdirnn0  15574  lgsdinn0  15575  gausslemma2dlem1a  15585  gausslemma2dlem6  15594  lgsquadlem1  15604  lgsquadlem2  15605  lgsquadlem3  15606  lgsquad2  15610  2lgslem3a1  15624  2lgslem3b1  15625  2lgslem3c1  15626  2lgslem3d1  15627  2lgsoddprmlem2  15633  2sqlem3  15644  2sqlem4  15645