Theorem mulcomd 8294

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 8255	. 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 2203  (class class class)co 6049   CCcc 8124   x. cmul 8131

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

This theorem is referenced by:  mul31  8403  remulext2  8873  mulreim  8877  mulext2  8886  mulcanapd  8934  mulcanap2d  8935  divcanap1  8954  divrecap2  8962  div23ap  8964  divdivdivap  8986  divmuleqap  8990  divadddivap  9000  apmul2  9062  apdivmuld  9086  divcanap5rd  9091  dmdcanap2d  9094  mvllmulapd  9115  prodgt0  9125  lt2mul2div  9152  mulle0r  9217  subhalfhalf  9472  qapne  9970  irrmulap  9979  mul2lt0llt0  10093  mul2lt0lgt0  10094  mul2lt0pn  10096  modqvalr  10686  modqcyc  10720  mulp1mod1  10726  modqmul12d  10739  modqnegd  10740  modqmulmodr  10751  addmodlteq  10759  expaddzap  10944  binom2  11012  binom3  11018  bccmpl  11115  bcm1k  11121  bcn2  11125  bcpasc  11127  cvg1nlemcxze  11663  cvg1nlemcau  11665  resqrexlemcalc1  11695  resqrexlemcalc2  11696  resqrexlemnm  11699  recvalap  11778  bdtrilem  11920  reccn2ap  11994  isummulc1  12109  fsummulc1  12131  trireciplem  12182  geolim  12193  cvgratnnlemnexp  12206  cvgratnnlemmn  12207  cvgratnnlemfm  12211  cvgratz  12214  mertensabs  12219  eftlub  12372  sinadd  12418  cosadd  12419  sin2t  12431  nndivides  12479  dvds2ln  12506  even2n  12556  oddm1even  12557  m1exp1  12583  divalgmod  12609  bitsp1  12633  bitsinv1lem  12643  mulgcdr  12710  rplpwr  12719  lcmgcdlem  12770  divgcdcoprmex  12795  cncongr1  12796  oddpwdclemxy  12862  2sqpwodd  12869  eulerthlema  12923  eulerthlemth  12925  prmdiv  12928  prmdivdiv  12930  modprmn0modprm0  12950  coprimeprodsq  12951  pythagtriplem6  12964  pythagtriplem7  12965  pceulem  12988  pcadd  13034  prmpwdvds  13049  mul4sqlem  13087  4sqlem17  13101  evenennn  13136  mulgassr  13869  znunit  14799  dvmulxxbr  15559  dvmptcmulcn  15578  dvply1  15622  tangtx  15695  cxpmul  15769  abscxp  15772  binom4  15836  pellexlem2  15838  wilthlem1  15840  mpodvdsmulf1o  15850  sgmppw  15852  perfect1  15858  lgsdirprm  15899  lgsdi  15902  lgsdirnn0  15912  lgsdinn0  15913  gausslemma2dlem1a  15923  gausslemma2dlem6  15932  lgsquadlem1  15942  lgsquadlem2  15943  lgsquadlem3  15944  lgsquad2  15948  2lgslem3a1  15962  2lgslem3b1  15963  2lgslem3c1  15964  2lgslem3d1  15965  2lgsoddprmlem2  15971  2sqlem3  15982  2sqlem4  15983