Theorem mulcomd 7901

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 7863	. 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 1335   e. wcel 2128  (class class class)co 5826   CCcc 7732   x. cmul 7739

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

This theorem is referenced by:  mul31  8010  remulext2  8479  mulreim  8483  mulext2  8492  mulcanapd  8539  mulcanap2d  8540  divcanap1  8558  divrecap2  8566  div23ap  8568  divdivdivap  8590  divmuleqap  8594  divadddivap  8604  apmul2  8666  apdivmuld  8690  divcanap5rd  8695  dmdcanap2d  8698  mvllmulapd  8719  prodgt0  8728  lt2mul2div  8755  mulle0r  8820  qapne  9554  mul2lt0llt0  9674  mul2lt0lgt0  9675  mul2lt0pn  9677  modqvalr  10233  modqcyc  10267  mulp1mod1  10273  modqmul12d  10286  modqnegd  10287  modqmulmodr  10298  addmodlteq  10306  expaddzap  10472  binom2  10538  binom3  10544  bccmpl  10639  bcm1k  10645  bcn2  10649  bcpasc  10651  cvg1nlemcxze  10893  cvg1nlemcau  10895  resqrexlemcalc1  10925  resqrexlemcalc2  10926  resqrexlemnm  10929  recvalap  11008  bdtrilem  11149  reccn2ap  11221  isummulc1  11335  fsummulc1  11357  trireciplem  11408  geolim  11419  cvgratnnlemnexp  11432  cvgratnnlemmn  11433  cvgratnnlemfm  11437  cvgratz  11440  mertensabs  11445  eftlub  11598  sinadd  11644  cosadd  11645  sin2t  11657  nndivides  11704  dvds2ln  11731  even2n  11777  oddm1even  11778  m1exp1  11804  divalgmod  11830  mulgcdr  11917  rplpwr  11926  lcmgcdlem  11969  divgcdcoprmex  11994  cncongr1  11995  oddpwdclemxy  12059  2sqpwodd  12066  eulerthlema  12120  eulerthlemth  12122  prmdiv  12125  prmdivdiv  12127  modprmn0modprm0  12146  coprimeprodsq  12147  pythagtriplem6  12160  pythagtriplem7  12161  pceulem  12184  evenennn  12192  dvmulxxbr  13136  dvmptcmulcn  13153  tangtx  13229  cxpmul  13303  abscxp  13305  binom4  13367