Theorem mulcomd 8065

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 8025	. 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 1364   e. wcel 2167  (class class class)co 5925   CCcc 7894   x. cmul 7901

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

This theorem is referenced by:  mul31  8174  remulext2  8644  mulreim  8648  mulext2  8657  mulcanapd  8705  mulcanap2d  8706  divcanap1  8725  divrecap2  8733  div23ap  8735  divdivdivap  8757  divmuleqap  8761  divadddivap  8771  apmul2  8833  apdivmuld  8857  divcanap5rd  8862  dmdcanap2d  8865  mvllmulapd  8886  prodgt0  8896  lt2mul2div  8923  mulle0r  8988  subhalfhalf  9243  qapne  9730  irrmulap  9739  mul2lt0llt0  9853  mul2lt0lgt0  9854  mul2lt0pn  9856  modqvalr  10434  modqcyc  10468  mulp1mod1  10474  modqmul12d  10487  modqnegd  10488  modqmulmodr  10499  addmodlteq  10507  expaddzap  10692  binom2  10760  binom3  10766  bccmpl  10863  bcm1k  10869  bcn2  10873  bcpasc  10875  cvg1nlemcxze  11164  cvg1nlemcau  11166  resqrexlemcalc1  11196  resqrexlemcalc2  11197  resqrexlemnm  11200  recvalap  11279  bdtrilem  11421  reccn2ap  11495  isummulc1  11609  fsummulc1  11631  trireciplem  11682  geolim  11693  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemfm  11711  cvgratz  11714  mertensabs  11719  eftlub  11872  sinadd  11918  cosadd  11919  sin2t  11931  nndivides  11979  dvds2ln  12006  even2n  12056  oddm1even  12057  m1exp1  12083  divalgmod  12109  bitsp1  12133  bitsinv1lem  12143  mulgcdr  12210  rplpwr  12219  lcmgcdlem  12270  divgcdcoprmex  12295  cncongr1  12296  oddpwdclemxy  12362  2sqpwodd  12369  eulerthlema  12423  eulerthlemth  12425  prmdiv  12428  prmdivdiv  12430  modprmn0modprm0  12450  coprimeprodsq  12451  pythagtriplem6  12464  pythagtriplem7  12465  pceulem  12488  pcadd  12534  prmpwdvds  12549  mul4sqlem  12587  4sqlem17  12601  evenennn  12635  mulgassr  13366  znunit  14291  dvmulxxbr  15022  dvmptcmulcn  15041  dvply1  15085  tangtx  15158  cxpmul  15232  abscxp  15235  binom4  15299  wilthlem1  15300  mpodvdsmulf1o  15310  sgmppw  15312  perfect1  15318  lgsdirprm  15359  lgsdi  15362  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1a  15383  gausslemma2dlem6  15392  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2  15408  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2lgsoddprmlem2  15431  2sqlem3  15442  2sqlem4  15443