Theorem mulcomd 7787

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   x. cmul 7625

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

This theorem is referenced by:  mul31  7893  remulext2  8362  mulreim  8366  mulext2  8375  mulcanapd  8422  mulcanap2d  8423  divcanap1  8441  divrecap2  8449  div23ap  8451  divdivdivap  8473  divmuleqap  8477  divadddivap  8487  apmul2  8549  apdivmuld  8573  divcanap5rd  8578  dmdcanap2d  8581  mvllmulapd  8601  prodgt0  8610  lt2mul2div  8637  mulle0r  8702  qapne  9431  mul2lt0llt0  9548  mul2lt0lgt0  9549  mul2lt0pn  9551  modqvalr  10098  modqcyc  10132  mulp1mod1  10138  modqmul12d  10151  modqnegd  10152  modqmulmodr  10163  addmodlteq  10171  expaddzap  10337  binom2  10403  binom3  10409  bccmpl  10500  bcm1k  10506  bcn2  10510  bcpasc  10512  cvg1nlemcxze  10754  cvg1nlemcau  10756  resqrexlemcalc1  10786  resqrexlemcalc2  10787  resqrexlemnm  10790  recvalap  10869  bdtrilem  11010  reccn2ap  11082  isummulc1  11196  fsummulc1  11218  trireciplem  11269  geolim  11280  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemfm  11298  cvgratz  11301  mertensabs  11306  eftlub  11396  sinadd  11443  cosadd  11444  sin2t  11456  nndivides  11500  dvds2ln  11526  even2n  11571  oddm1even  11572  m1exp1  11598  divalgmod  11624  mulgcdr  11706  rplpwr  11715  lcmgcdlem  11758  divgcdcoprmex  11783  cncongr1  11784  oddpwdclemxy  11847  2sqpwodd  11854  evenennn  11906  dvmulxxbr  12835  dvmptcmulcn  12852  tangtx  12919