Theorem mulcomd 8201

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 8161	. 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 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   x. cmul 8037

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

This theorem is referenced by:  mul31  8310  remulext2  8780  mulreim  8784  mulext2  8793  mulcanapd  8841  mulcanap2d  8842  divcanap1  8861  divrecap2  8869  div23ap  8871  divdivdivap  8893  divmuleqap  8897  divadddivap  8907  apmul2  8969  apdivmuld  8993  divcanap5rd  8998  dmdcanap2d  9001  mvllmulapd  9022  prodgt0  9032  lt2mul2div  9059  mulle0r  9124  subhalfhalf  9379  qapne  9873  irrmulap  9882  mul2lt0llt0  9996  mul2lt0lgt0  9997  mul2lt0pn  9999  modqvalr  10588  modqcyc  10622  mulp1mod1  10628  modqmul12d  10641  modqnegd  10642  modqmulmodr  10653  addmodlteq  10661  expaddzap  10846  binom2  10914  binom3  10920  bccmpl  11017  bcm1k  11023  bcn2  11027  bcpasc  11029  cvg1nlemcxze  11547  cvg1nlemcau  11549  resqrexlemcalc1  11579  resqrexlemcalc2  11580  resqrexlemnm  11583  recvalap  11662  bdtrilem  11804  reccn2ap  11878  isummulc1  11993  fsummulc1  12015  trireciplem  12066  geolim  12077  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  cvgratnnlemfm  12095  cvgratz  12098  mertensabs  12103  eftlub  12256  sinadd  12302  cosadd  12303  sin2t  12315  nndivides  12363  dvds2ln  12390  even2n  12440  oddm1even  12441  m1exp1  12467  divalgmod  12493  bitsp1  12517  bitsinv1lem  12527  mulgcdr  12594  rplpwr  12603  lcmgcdlem  12654  divgcdcoprmex  12679  cncongr1  12680  oddpwdclemxy  12746  2sqpwodd  12753  eulerthlema  12807  eulerthlemth  12809  prmdiv  12812  prmdivdiv  12814  modprmn0modprm0  12834  coprimeprodsq  12835  pythagtriplem6  12848  pythagtriplem7  12849  pceulem  12872  pcadd  12918  prmpwdvds  12933  mul4sqlem  12971  4sqlem17  12985  evenennn  13019  mulgassr  13752  znunit  14679  dvmulxxbr  15432  dvmptcmulcn  15451  dvply1  15495  tangtx  15568  cxpmul  15642  abscxp  15645  binom4  15709  wilthlem1  15710  mpodvdsmulf1o  15720  sgmppw  15722  perfect1  15728  lgsdirprm  15769  lgsdi  15772  lgsdirnn0  15782  lgsdinn0  15783  gausslemma2dlem1a  15793  gausslemma2dlem6  15802  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2  15818  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgslem3d1  15835  2lgsoddprmlem2  15841  2sqlem3  15852  2sqlem4  15853