Theorem mulcomd 8067

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 8027	. 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 1364   e. wcel 2167  (class class class)co 5925   CCcc 7896   x. cmul 7903

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

This theorem is referenced by:  mul31  8176  remulext2  8646  mulreim  8650  mulext2  8659  mulcanapd  8707  mulcanap2d  8708  divcanap1  8727  divrecap2  8735  div23ap  8737  divdivdivap  8759  divmuleqap  8763  divadddivap  8773  apmul2  8835  apdivmuld  8859  divcanap5rd  8864  dmdcanap2d  8867  mvllmulapd  8888  prodgt0  8898  lt2mul2div  8925  mulle0r  8990  subhalfhalf  9245  qapne  9732  irrmulap  9741  mul2lt0llt0  9855  mul2lt0lgt0  9856  mul2lt0pn  9858  modqvalr  10436  modqcyc  10470  mulp1mod1  10476  modqmul12d  10489  modqnegd  10490  modqmulmodr  10501  addmodlteq  10509  expaddzap  10694  binom2  10762  binom3  10768  bccmpl  10865  bcm1k  10871  bcn2  10875  bcpasc  10877  cvg1nlemcxze  11166  cvg1nlemcau  11168  resqrexlemcalc1  11198  resqrexlemcalc2  11199  resqrexlemnm  11202  recvalap  11281  bdtrilem  11423  reccn2ap  11497  isummulc1  11611  fsummulc1  11633  trireciplem  11684  geolim  11695  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemfm  11713  cvgratz  11716  mertensabs  11721  eftlub  11874  sinadd  11920  cosadd  11921  sin2t  11933  nndivides  11981  dvds2ln  12008  even2n  12058  oddm1even  12059  m1exp1  12085  divalgmod  12111  bitsp1  12135  bitsinv1lem  12145  mulgcdr  12212  rplpwr  12221  lcmgcdlem  12272  divgcdcoprmex  12297  cncongr1  12298  oddpwdclemxy  12364  2sqpwodd  12371  eulerthlema  12425  eulerthlemth  12427  prmdiv  12430  prmdivdiv  12432  modprmn0modprm0  12452  coprimeprodsq  12453  pythagtriplem6  12466  pythagtriplem7  12467  pceulem  12490  pcadd  12536  prmpwdvds  12551  mul4sqlem  12589  4sqlem17  12603  evenennn  12637  mulgassr  13368  znunit  14293  dvmulxxbr  15046  dvmptcmulcn  15065  dvply1  15109  tangtx  15182  cxpmul  15256  abscxp  15259  binom4  15323  wilthlem1  15324  mpodvdsmulf1o  15334  sgmppw  15336  perfect1  15342  lgsdirprm  15383  lgsdi  15386  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1a  15407  gausslemma2dlem6  15416  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2  15432  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  2lgsoddprmlem2  15455  2sqlem3  15466  2sqlem4  15467