Theorem mulcomd 7941

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 7903	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4	1, 2, 3	syl2anc 409	1 |- ( ph -> ( A x. B ) = ( B x. A ) )

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   x. cmul 7779

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

This theorem is referenced by:  mul31  8050  remulext2  8519  mulreim  8523  mulext2  8532  mulcanapd  8579  mulcanap2d  8580  divcanap1  8598  divrecap2  8606  div23ap  8608  divdivdivap  8630  divmuleqap  8634  divadddivap  8644  apmul2  8706  apdivmuld  8730  divcanap5rd  8735  dmdcanap2d  8738  mvllmulapd  8759  prodgt0  8768  lt2mul2div  8795  mulle0r  8860  qapne  9598  mul2lt0llt0  9718  mul2lt0lgt0  9719  mul2lt0pn  9721  modqvalr  10281  modqcyc  10315  mulp1mod1  10321  modqmul12d  10334  modqnegd  10335  modqmulmodr  10346  addmodlteq  10354  expaddzap  10520  binom2  10587  binom3  10593  bccmpl  10688  bcm1k  10694  bcn2  10698  bcpasc  10700  cvg1nlemcxze  10946  cvg1nlemcau  10948  resqrexlemcalc1  10978  resqrexlemcalc2  10979  resqrexlemnm  10982  recvalap  11061  bdtrilem  11202  reccn2ap  11276  isummulc1  11390  fsummulc1  11412  trireciplem  11463  geolim  11474  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemfm  11492  cvgratz  11495  mertensabs  11500  eftlub  11653  sinadd  11699  cosadd  11700  sin2t  11712  nndivides  11759  dvds2ln  11786  even2n  11833  oddm1even  11834  m1exp1  11860  divalgmod  11886  mulgcdr  11973  rplpwr  11982  lcmgcdlem  12031  divgcdcoprmex  12056  cncongr1  12057  oddpwdclemxy  12123  2sqpwodd  12130  eulerthlema  12184  eulerthlemth  12186  prmdiv  12189  prmdivdiv  12191  modprmn0modprm0  12210  coprimeprodsq  12211  pythagtriplem6  12224  pythagtriplem7  12225  pceulem  12248  pcadd  12293  prmpwdvds  12307  mul4sqlem  12345  evenennn  12348  dvmulxxbr  13460  dvmptcmulcn  13477  tangtx  13553  cxpmul  13627  abscxp  13629  binom4  13691  lgsdirprm  13729  lgsdi  13732  lgsdirnn0  13742  lgsdinn0  13743  2sqlem3  13747  2sqlem4  13748