Theorem mulcomd 8311

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 8272	. 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 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   x. cmul 8148

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

This theorem is referenced by:  mul31  8420  remulext2  8891  mulreim  8895  mulext2  8904  mulcanapd  8952  mulcanap2d  8953  divcanap1  8972  divrecap2  8980  div23ap  8982  divdivdivap  9004  divmuleqap  9008  divadddivap  9018  apmul2  9080  apdivmuld  9104  divcanap5rd  9109  dmdcanap2d  9112  mvllmulapd  9133  prodgt0  9143  lt2mul2div  9170  mulle0r  9235  subhalfhalf  9490  qapne  9989  irrmulap  9998  mul2lt0llt0  10112  mul2lt0lgt0  10113  mul2lt0pn  10115  modqvalr  10711  modqcyc  10745  mulp1mod1  10751  modqmul12d  10764  modqnegd  10765  modqmulmodr  10776  addmodlteq  10784  expaddzap  10969  binom2  11037  binom3  11043  bccmpl  11141  bcm1k  11147  bcn2  11151  bcpasc  11153  cvg1nlemcxze  11692  cvg1nlemcau  11694  resqrexlemcalc1  11724  resqrexlemcalc2  11725  resqrexlemnm  11728  recvalap  11807  bdtrilem  11949  reccn2ap  12023  isummulc1  12138  fsummulc1  12160  trireciplem  12211  geolim  12222  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemfm  12240  cvgratz  12243  mertensabs  12248  eftlub  12401  sinadd  12447  cosadd  12448  sin2t  12460  nndivides  12508  dvds2ln  12535  even2n  12585  oddm1even  12586  m1exp1  12612  divalgmod  12638  bitsp1  12662  bitsinv1lem  12672  mulgcdr  12739  rplpwr  12748  lcmgcdlem  12799  divgcdcoprmex  12824  cncongr1  12825  oddpwdclemxy  12891  2sqpwodd  12898  eulerthlema  12952  eulerthlemth  12954  prmdiv  12957  prmdivdiv  12959  modprmn0modprm0  12979  coprimeprodsq  12980  pythagtriplem6  12993  pythagtriplem7  12994  pceulem  13017  pcadd  13063  prmpwdvds  13078  mul4sqlem  13116  4sqlem17  13130  evenennn  13228  mulgassr  13961  znunit  14919  dvmulxxbr  15679  dvmptcmulcn  15698  dvply1  15742  tangtx  15815  cxpmul  15889  abscxp  15892  binom4  15956  pellexlem2  15958  wilthlem1  15960  mpodvdsmulf1o  15970  sgmppw  15972  perfect1  15978  lgsdirprm  16019  lgsdi  16022  lgsdirnn0  16032  lgsdinn0  16033  gausslemma2dlem1a  16043  gausslemma2dlem6  16052  lgsquadlem1  16062  lgsquadlem2  16063  lgsquadlem3  16064  lgsquad2  16068  2lgslem3a1  16082  2lgslem3b1  16083  2lgslem3c1  16084  2lgslem3d1  16085  2lgsoddprmlem2  16091  2sqlem3  16102  2sqlem4  16103