Theorem addcom 7899

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   + caddc 7623

This theorem was proved from axioms:  ax-addcom 7720

This theorem is referenced by:  addid2  7901  readdcan  7902  addcomi  7906  addcomd  7913  add12  7920  add32  7921  add42  7924  cnegexlem1  7937  cnegexlem3  7939  cnegex2  7941  subsub23  7967  pncan2  7969  addsub  7973  addsub12  7975  addsubeq4  7977  sub32  7996  pnpcan2  8002  ppncan  8004  sub4  8007  negsubdi2  8021  ltadd2  8181  ltaddnegr  8187  ltaddsub2  8199  leaddsub2  8201  leltadd  8209  ltaddpos2  8215  addge02  8235  conjmulap  8489  recreclt  8658  avgle1  8960  avgle2  8961  nn0nnaddcl  9008  xaddcom  9644  fzen  9823  fzshftral  9888  flqzadd  10071  addmodidr  10146  nn0ennn  10206  ser3add  10278  bernneq2  10413  shftval2  10598  shftval4  10600  crim  10630  resqrexlemover  10782  climshft2  11075  summodclem3  11149  binom1dif  11256  isumshft  11259  arisum  11267  mertenslemi1  11304  addcos  11453  demoivreALT  11480  dvdsaddr  11537  divalgb  11622  hashdvds  11897  ioo2bl  12712  ptolemy  12905