Theorem mulcomd 7780

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 7742	. 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 5767   CCcc 7611   x. cmul 7618

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

This theorem is referenced by:  mul31  7886  remulext2  8355  mulreim  8359  mulext2  8368  mulcanapd  8415  mulcanap2d  8416  divcanap1  8434  divrecap2  8442  div23ap  8444  divdivdivap  8466  divmuleqap  8470  divadddivap  8480  apmul2  8542  apdivmuld  8566  divcanap5rd  8571  dmdcanap2d  8574  mvllmulapd  8594  prodgt0  8603  lt2mul2div  8630  mulle0r  8695  qapne  9424  mul2lt0llt0  9541  mul2lt0lgt0  9542  mul2lt0pn  9544  modqvalr  10091  modqcyc  10125  mulp1mod1  10131  modqmul12d  10144  modqnegd  10145  modqmulmodr  10156  addmodlteq  10164  expaddzap  10330  binom2  10396  binom3  10402  bccmpl  10493  bcm1k  10499  bcn2  10503  bcpasc  10505  cvg1nlemcxze  10747  cvg1nlemcau  10749  resqrexlemcalc1  10779  resqrexlemcalc2  10780  resqrexlemnm  10783  recvalap  10862  bdtrilem  11003  reccn2ap  11075  isummulc1  11189  fsummulc1  11211  trireciplem  11262  geolim  11273  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemfm  11291  cvgratz  11294  mertensabs  11299  eftlub  11385  sinadd  11432  cosadd  11433  sin2t  11445  nndivides  11489  dvds2ln  11515  even2n  11560  oddm1even  11561  m1exp1  11587  divalgmod  11613  mulgcdr  11695  rplpwr  11704  lcmgcdlem  11747  divgcdcoprmex  11772  cncongr1  11773  oddpwdclemxy  11836  2sqpwodd  11843  evenennn  11895  dvmulxxbr  12824  dvmptcmulcn  12841  tangtx  12908