Theorem mulcomd 8311

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 8272	. 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 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   x. cmul 8148

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

This theorem is referenced by:  mul31  8421  remulext2  8892  mulreim  8896  mulext2  8905  mulcanapd  8953  mulcanap2d  8954  divcanap1  8975  divrecap2  8983  div23ap  8985  divdivdivap  9007  divmuleqap  9011  divadddivap  9021  apmul2  9083  apdivmuld  9107  divcanap5rd  9112  dmdcanap2d  9115  mvllmulapd  9136  prodgt0  9146  lt2mul2div  9173  mulle0r  9238  subhalfhalf  9493  qapne  9992  irrmulap  10001  mul2lt0llt0  10115  mul2lt0lgt0  10116  mul2lt0pn  10118  modqvalr  10714  modqcyc  10748  mulp1mod1  10754  modqmul12d  10767  modqnegd  10768  modqmulmodr  10779  addmodlteq  10787  expaddzap  10972  binom2  11040  binom3  11046  bccmpl  11144  bcm1k  11150  bcn2  11154  bcpasc  11156  cvg1nlemcxze  11696  cvg1nlemcau  11698  resqrexlemcalc1  11728  resqrexlemcalc2  11729  resqrexlemnm  11732  recvalap  11811  bdtrilem  11953  reccn2ap  12027  isummulc1  12142  fsummulc1  12164  trireciplem  12215  geolim  12226  cvgratnnlemnexp  12239  cvgratnnlemmn  12240  cvgratnnlemfm  12244  cvgratz  12247  mertensabs  12252  eftlub  12405  sinadd  12451  cosadd  12452  sin2t  12464  nndivides  12512  dvds2ln  12539  even2n  12589  oddm1even  12590  m1exp1  12616  divalgmod  12642  bitsp1  12666  bitsinv1lem  12676  mulgcdr  12743  rplpwr  12752  lcmgcdlem  12803  divgcdcoprmex  12828  cncongr1  12829  oddpwdclemxy  12895  2sqpwodd  12902  eulerthlema  12956  eulerthlemth  12958  prmdiv  12961  prmdivdiv  12963  modprmn0modprm0  12983  coprimeprodsq  12984  pythagtriplem6  12997  pythagtriplem7  12998  pceulem  13021  pcadd  13067  prmpwdvds  13082  mul4sqlem  13120  4sqlem17  13134  evenennn  13232  mulgassr  13917  znunit  14937  dvmulxxbr  15697  dvmptcmulcn  15716  dvply1  15760  tangtx  15833  cxpmul  15907  abscxp  15910  binom4  15974  pellexlem2  15976  wilthlem1  15978  mpodvdsmulf1o  15988  sgmppw  15990  perfect1  15996  lgsdirprm  16037  lgsdi  16040  lgsdirnn0  16050  lgsdinn0  16051  gausslemma2dlem1a  16061  gausslemma2dlem6  16070  lgsquadlem1  16080  lgsquadlem2  16081  lgsquadlem3  16082  lgsquad2  16086  2lgslem3a1  16100  2lgslem3b1  16101  2lgslem3c1  16102  2lgslem3d1  16103  2lgsoddprmlem2  16109  2sqlem3  16120  2sqlem4  16121  dichmul0orlem3  16639