Theorem addcom 8068

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   e. wcel 2146  (class class class)co 5865   CCcc 7784   + caddc 7789

This theorem was proved from axioms:  ax-addcom 7886

This theorem is referenced by:  addid2  8070  readdcan  8071  addcomi  8075  addcomd  8082  add12  8089  add32  8090  add42  8093  cnegexlem1  8106  cnegexlem3  8108  cnegex2  8110  subsub23  8136  pncan2  8138  addsub  8142  addsub12  8144  addsubeq4  8146  sub32  8165  pnpcan2  8171  ppncan  8173  sub4  8176  negsubdi2  8190  ltadd2  8350  ltaddnegr  8356  ltaddsub2  8368  leaddsub2  8370  leltadd  8378  ltaddpos2  8384  addge02  8404  conjmulap  8658  recreclt  8828  avgle1  9130  avgle2  9131  nn0nnaddcl  9178  xaddcom  9830  fzen  10011  fzshftral  10076  flqzadd  10266  addmodidr  10341  nn0ennn  10401  ser3add  10473  bernneq2  10609  shftval2  10801  shftval4  10803  crim  10833  resqrexlemover  10985  climshft2  11280  summodclem3  11354  binom1dif  11461  isumshft  11464  arisum  11472  mertenslemi1  11509  addcos  11720  demoivreALT  11747  dvdsaddr  11810  divalgb  11895  hashdvds  12186  pythagtriplem2  12231  mulgnndir  12870  ioo2bl  13594  reeff1olem  13743  ptolemy  13796