Theorem addcom 8094

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   e. wcel 2148  (class class class)co 5875   CCcc 7809   + caddc 7814

This theorem was proved from axioms:  ax-addcom 7911

This theorem is referenced by:  addlid  8096  readdcan  8097  addcomi  8101  addcomd  8108  add12  8115  add32  8116  add42  8119  cnegexlem1  8132  cnegexlem3  8134  cnegex2  8136  subsub23  8162  pncan2  8164  addsub  8168  addsub12  8170  addsubeq4  8172  sub32  8191  pnpcan2  8197  ppncan  8199  sub4  8202  negsubdi2  8216  ltadd2  8376  ltaddnegr  8382  ltaddsub2  8394  leaddsub2  8396  leltadd  8404  ltaddpos2  8410  addge02  8430  conjmulap  8686  recreclt  8857  avgle1  9159  avgle2  9160  nn0nnaddcl  9207  xaddcom  9861  fzen  10043  fzshftral  10108  flqzadd  10298  addmodidr  10373  nn0ennn  10433  ser3add  10505  bernneq2  10642  shftval2  10835  shftval4  10837  crim  10867  resqrexlemover  11019  climshft2  11314  summodclem3  11388  binom1dif  11495  isumshft  11498  arisum  11506  mertenslemi1  11543  addcos  11754  demoivreALT  11781  dvdsaddr  11844  divalgb  11930  hashdvds  12221  pythagtriplem2  12266  mulgnndir  13012  cncrng  13466  ioo2bl  14046  reeff1olem  14195  ptolemy  14248