Theorem mulcomd 8244

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 8204	. 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 2202  (class class class)co 6028   CCcc 8073   x. cmul 8080

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

This theorem is referenced by:  mul31  8353  remulext2  8823  mulreim  8827  mulext2  8836  mulcanapd  8884  mulcanap2d  8885  divcanap1  8904  divrecap2  8912  div23ap  8914  divdivdivap  8936  divmuleqap  8940  divadddivap  8950  apmul2  9012  apdivmuld  9036  divcanap5rd  9041  dmdcanap2d  9044  mvllmulapd  9065  prodgt0  9075  lt2mul2div  9102  mulle0r  9167  subhalfhalf  9422  qapne  9916  irrmulap  9925  mul2lt0llt0  10039  mul2lt0lgt0  10040  mul2lt0pn  10042  modqvalr  10631  modqcyc  10665  mulp1mod1  10671  modqmul12d  10684  modqnegd  10685  modqmulmodr  10696  addmodlteq  10704  expaddzap  10889  binom2  10957  binom3  10963  bccmpl  11060  bcm1k  11066  bcn2  11070  bcpasc  11072  cvg1nlemcxze  11603  cvg1nlemcau  11605  resqrexlemcalc1  11635  resqrexlemcalc2  11636  resqrexlemnm  11639  recvalap  11718  bdtrilem  11860  reccn2ap  11934  isummulc1  12049  fsummulc1  12071  trireciplem  12122  geolim  12133  cvgratnnlemnexp  12146  cvgratnnlemmn  12147  cvgratnnlemfm  12151  cvgratz  12154  mertensabs  12159  eftlub  12312  sinadd  12358  cosadd  12359  sin2t  12371  nndivides  12419  dvds2ln  12446  even2n  12496  oddm1even  12497  m1exp1  12523  divalgmod  12549  bitsp1  12573  bitsinv1lem  12583  mulgcdr  12650  rplpwr  12659  lcmgcdlem  12710  divgcdcoprmex  12735  cncongr1  12736  oddpwdclemxy  12802  2sqpwodd  12809  eulerthlema  12863  eulerthlemth  12865  prmdiv  12868  prmdivdiv  12870  modprmn0modprm0  12890  coprimeprodsq  12891  pythagtriplem6  12904  pythagtriplem7  12905  pceulem  12928  pcadd  12974  prmpwdvds  12989  mul4sqlem  13027  4sqlem17  13041  evenennn  13075  mulgassr  13808  znunit  14735  dvmulxxbr  15493  dvmptcmulcn  15512  dvply1  15556  tangtx  15629  cxpmul  15703  abscxp  15706  binom4  15770  pellexlem2  15772  wilthlem1  15774  mpodvdsmulf1o  15784  sgmppw  15786  perfect1  15792  lgsdirprm  15833  lgsdi  15836  lgsdirnn0  15846  lgsdinn0  15847  gausslemma2dlem1a  15857  gausslemma2dlem6  15866  lgsquadlem1  15876  lgsquadlem2  15877  lgsquadlem3  15878  lgsquad2  15882  2lgslem3a1  15896  2lgslem3b1  15897  2lgslem3c1  15898  2lgslem3d1  15899  2lgsoddprmlem2  15905  2sqlem3  15916  2sqlem4  15917