Theorem mulcomd 7981

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 7942	. 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 1353   e. wcel 2148  (class class class)co 5877   CCcc 7811   x. cmul 7818

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

This theorem is referenced by:  mul31  8090  remulext2  8559  mulreim  8563  mulext2  8572  mulcanapd  8620  mulcanap2d  8621  divcanap1  8640  divrecap2  8648  div23ap  8650  divdivdivap  8672  divmuleqap  8676  divadddivap  8686  apmul2  8748  apdivmuld  8772  divcanap5rd  8777  dmdcanap2d  8780  mvllmulapd  8801  prodgt0  8811  lt2mul2div  8838  mulle0r  8903  qapne  9641  mul2lt0llt0  9763  mul2lt0lgt0  9764  mul2lt0pn  9766  modqvalr  10327  modqcyc  10361  mulp1mod1  10367  modqmul12d  10380  modqnegd  10381  modqmulmodr  10392  addmodlteq  10400  expaddzap  10566  binom2  10634  binom3  10640  bccmpl  10736  bcm1k  10742  bcn2  10746  bcpasc  10748  cvg1nlemcxze  10993  cvg1nlemcau  10995  resqrexlemcalc1  11025  resqrexlemcalc2  11026  resqrexlemnm  11029  recvalap  11108  bdtrilem  11249  reccn2ap  11323  isummulc1  11437  fsummulc1  11459  trireciplem  11510  geolim  11521  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratnnlemfm  11539  cvgratz  11542  mertensabs  11547  eftlub  11700  sinadd  11746  cosadd  11747  sin2t  11759  nndivides  11806  dvds2ln  11833  even2n  11881  oddm1even  11882  m1exp1  11908  divalgmod  11934  mulgcdr  12021  rplpwr  12030  lcmgcdlem  12079  divgcdcoprmex  12104  cncongr1  12105  oddpwdclemxy  12171  2sqpwodd  12178  eulerthlema  12232  eulerthlemth  12234  prmdiv  12237  prmdivdiv  12239  modprmn0modprm0  12258  coprimeprodsq  12259  pythagtriplem6  12272  pythagtriplem7  12273  pceulem  12296  pcadd  12341  prmpwdvds  12355  mul4sqlem  12393  evenennn  12396  mulgassr  13026  dvmulxxbr  14251  dvmptcmulcn  14268  tangtx  14344  cxpmul  14418  abscxp  14420  binom4  14482  lgsdirprm  14520  lgsdi  14523  lgsdirnn0  14533  lgsdinn0  14534  2lgsoddprmlem2  14539  2sqlem3  14549  2sqlem4  14550