Theorem addcom 8209

Description: Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)

Assertion

Ref	Expression
addcom	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )

Proof of Theorem addcom

Step	Hyp	Ref	Expression
1		ax-addcom 8025	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   e. wcel 2176  (class class class)co 5944   CCcc 7923   + caddc 7928

This theorem was proved from axioms:  ax-addcom 8025

This theorem is referenced by:  addlid  8211  readdcan  8212  addcomi  8216  addcomd  8223  add12  8230  add32  8231  add42  8234  cnegexlem1  8247  cnegexlem3  8249  cnegex2  8251  subsub23  8277  pncan2  8279  addsub  8283  addsub12  8285  addsubeq4  8287  sub32  8306  pnpcan2  8312  ppncan  8314  sub4  8317  negsubdi2  8331  ltadd2  8492  ltaddnegr  8498  ltaddsub2  8510  leaddsub2  8512  leltadd  8520  ltaddpos2  8526  addge02  8546  conjmulap  8802  recreclt  8973  avgle1  9278  avgle2  9279  nn0nnaddcl  9326  xaddcom  9983  fzen  10165  fzshftral  10230  fzo0addelr  10318  flqzadd  10441  addmodidr  10518  nn0ennn  10578  ser3add  10667  bernneq2  10806  ccatrn  11065  shftval2  11137  shftval4  11139  crim  11169  resqrexlemover  11321  climshft2  11617  summodclem3  11691  binom1dif  11798  isumshft  11801  arisum  11809  mertenslemi1  11846  addcos  12057  demoivreALT  12085  dvdsaddr  12148  divalgb  12236  hashdvds  12543  pythagtriplem2  12589  mulgnndir  13487  cncrng  14331  ioo2bl  15023  reeff1olem  15243  ptolemy  15296  wilthlem1  15452  1sgmprm  15466  perfectlem2  15472