Theorem addcom 8056

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   + caddc 7777

This theorem was proved from axioms:  ax-addcom 7874

This theorem is referenced by:  addid2  8058  readdcan  8059  addcomi  8063  addcomd  8070  add12  8077  add32  8078  add42  8081  cnegexlem1  8094  cnegexlem3  8096  cnegex2  8098  subsub23  8124  pncan2  8126  addsub  8130  addsub12  8132  addsubeq4  8134  sub32  8153  pnpcan2  8159  ppncan  8161  sub4  8164  negsubdi2  8178  ltadd2  8338  ltaddnegr  8344  ltaddsub2  8356  leaddsub2  8358  leltadd  8366  ltaddpos2  8372  addge02  8392  conjmulap  8646  recreclt  8816  avgle1  9118  avgle2  9119  nn0nnaddcl  9166  xaddcom  9818  fzen  9999  fzshftral  10064  flqzadd  10254  addmodidr  10329  nn0ennn  10389  ser3add  10461  bernneq2  10597  shftval2  10790  shftval4  10792  crim  10822  resqrexlemover  10974  climshft2  11269  summodclem3  11343  binom1dif  11450  isumshft  11453  arisum  11461  mertenslemi1  11498  addcos  11709  demoivreALT  11736  dvdsaddr  11799  divalgb  11884  hashdvds  12175  pythagtriplem2  12220  ioo2bl  13337  reeff1olem  13486  ptolemy  13539