Theorem mulcomd 7916

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 7878	. 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 1343   e. wcel 2136  (class class class)co 5841   CCcc 7747   x. cmul 7754

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

This theorem is referenced by:  mul31  8025  remulext2  8494  mulreim  8498  mulext2  8507  mulcanapd  8554  mulcanap2d  8555  divcanap1  8573  divrecap2  8581  div23ap  8583  divdivdivap  8605  divmuleqap  8609  divadddivap  8619  apmul2  8681  apdivmuld  8705  divcanap5rd  8710  dmdcanap2d  8713  mvllmulapd  8734  prodgt0  8743  lt2mul2div  8770  mulle0r  8835  qapne  9573  mul2lt0llt0  9693  mul2lt0lgt0  9694  mul2lt0pn  9696  modqvalr  10256  modqcyc  10290  mulp1mod1  10296  modqmul12d  10309  modqnegd  10310  modqmulmodr  10321  addmodlteq  10329  expaddzap  10495  binom2  10562  binom3  10568  bccmpl  10663  bcm1k  10669  bcn2  10673  bcpasc  10675  cvg1nlemcxze  10920  cvg1nlemcau  10922  resqrexlemcalc1  10952  resqrexlemcalc2  10953  resqrexlemnm  10956  recvalap  11035  bdtrilem  11176  reccn2ap  11250  isummulc1  11364  fsummulc1  11386  trireciplem  11437  geolim  11448  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemfm  11466  cvgratz  11469  mertensabs  11474  eftlub  11627  sinadd  11673  cosadd  11674  sin2t  11686  nndivides  11733  dvds2ln  11760  even2n  11807  oddm1even  11808  m1exp1  11834  divalgmod  11860  mulgcdr  11947  rplpwr  11956  lcmgcdlem  12005  divgcdcoprmex  12030  cncongr1  12031  oddpwdclemxy  12097  2sqpwodd  12104  eulerthlema  12158  eulerthlemth  12160  prmdiv  12163  prmdivdiv  12165  modprmn0modprm0  12184  coprimeprodsq  12185  pythagtriplem6  12198  pythagtriplem7  12199  pceulem  12222  pcadd  12267  prmpwdvds  12281  mul4sqlem  12319  evenennn  12322  dvmulxxbr  13266  dvmptcmulcn  13283  tangtx  13359  cxpmul  13433  abscxp  13435  binom4  13497  lgsdirprm  13535  lgsdi  13538  lgsdirnn0  13548  lgsdinn0  13549  2sqlem3  13553  2sqlem4  13554