Theorem mulcomd 8156

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 8116	. 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 1395   e. wcel 2200  (class class class)co 5994   CCcc 7985   x. cmul 7992

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

This theorem is referenced by:  mul31  8265  remulext2  8735  mulreim  8739  mulext2  8748  mulcanapd  8796  mulcanap2d  8797  divcanap1  8816  divrecap2  8824  div23ap  8826  divdivdivap  8848  divmuleqap  8852  divadddivap  8862  apmul2  8924  apdivmuld  8948  divcanap5rd  8953  dmdcanap2d  8956  mvllmulapd  8977  prodgt0  8987  lt2mul2div  9014  mulle0r  9079  subhalfhalf  9334  qapne  9822  irrmulap  9831  mul2lt0llt0  9945  mul2lt0lgt0  9946  mul2lt0pn  9948  modqvalr  10534  modqcyc  10568  mulp1mod1  10574  modqmul12d  10587  modqnegd  10588  modqmulmodr  10599  addmodlteq  10607  expaddzap  10792  binom2  10860  binom3  10866  bccmpl  10963  bcm1k  10969  bcn2  10973  bcpasc  10975  cvg1nlemcxze  11479  cvg1nlemcau  11481  resqrexlemcalc1  11511  resqrexlemcalc2  11512  resqrexlemnm  11515  recvalap  11594  bdtrilem  11736  reccn2ap  11810  isummulc1  11924  fsummulc1  11946  trireciplem  11997  geolim  12008  cvgratnnlemnexp  12021  cvgratnnlemmn  12022  cvgratnnlemfm  12026  cvgratz  12029  mertensabs  12034  eftlub  12187  sinadd  12233  cosadd  12234  sin2t  12246  nndivides  12294  dvds2ln  12321  even2n  12371  oddm1even  12372  m1exp1  12398  divalgmod  12424  bitsp1  12448  bitsinv1lem  12458  mulgcdr  12525  rplpwr  12534  lcmgcdlem  12585  divgcdcoprmex  12610  cncongr1  12611  oddpwdclemxy  12677  2sqpwodd  12684  eulerthlema  12738  eulerthlemth  12740  prmdiv  12743  prmdivdiv  12745  modprmn0modprm0  12765  coprimeprodsq  12766  pythagtriplem6  12779  pythagtriplem7  12780  pceulem  12803  pcadd  12849  prmpwdvds  12864  mul4sqlem  12902  4sqlem17  12916  evenennn  12950  mulgassr  13683  znunit  14608  dvmulxxbr  15361  dvmptcmulcn  15380  dvply1  15424  tangtx  15497  cxpmul  15571  abscxp  15574  binom4  15638  wilthlem1  15639  mpodvdsmulf1o  15649  sgmppw  15651  perfect1  15657  lgsdirprm  15698  lgsdi  15701  lgsdirnn0  15711  lgsdinn0  15712  gausslemma2dlem1a  15722  gausslemma2dlem6  15731  lgsquadlem1  15741  lgsquadlem2  15742  lgsquadlem3  15743  lgsquad2  15747  2lgslem3a1  15761  2lgslem3b1  15762  2lgslem3c1  15763  2lgslem3d1  15764  2lgsoddprmlem2  15770  2sqlem3  15781  2sqlem4  15782