Theorem addcom 8315

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 8131	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   + caddc 8034

This theorem was proved from axioms:  ax-addcom 8131

This theorem is referenced by:  addlid  8317  readdcan  8318  addcomi  8322  addcomd  8329  add12  8336  add32  8337  add42  8340  cnegexlem1  8353  cnegexlem3  8355  cnegex2  8357  subsub23  8383  pncan2  8385  addsub  8389  addsub12  8391  addsubeq4  8393  sub32  8412  pnpcan2  8418  ppncan  8420  sub4  8423  negsubdi2  8437  ltadd2  8598  ltaddnegr  8604  ltaddsub2  8616  leaddsub2  8618  leltadd  8626  ltaddpos2  8632  addge02  8652  conjmulap  8908  recreclt  9079  avgle1  9384  avgle2  9385  nn0nnaddcl  9432  xaddcom  10095  fzen  10277  fzshftral  10342  fzo0addelr  10433  flqzadd  10557  addmodidr  10634  nn0ennn  10694  ser3add  10783  bernneq2  10922  ccatrn  11185  ccatalpha  11189  shftval2  11386  shftval4  11388  crim  11418  resqrexlemover  11570  climshft2  11866  summodclem3  11940  binom1dif  12047  isumshft  12050  arisum  12058  mertenslemi1  12095  addcos  12306  demoivreALT  12334  dvdsaddr  12397  divalgb  12485  hashdvds  12792  pythagtriplem2  12838  mulgnndir  13737  cncrng  14582  ioo2bl  15274  reeff1olem  15494  ptolemy  15547  wilthlem1  15703  1sgmprm  15717  perfectlem2  15723