Theorem addcom 7923

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1332   e. wcel 1481  (class class class)co 5782   CCcc 7642   + caddc 7647

This theorem was proved from axioms:  ax-addcom 7744

This theorem is referenced by:  addid2  7925  readdcan  7926  addcomi  7930  addcomd  7937  add12  7944  add32  7945  add42  7948  cnegexlem1  7961  cnegexlem3  7963  cnegex2  7965  subsub23  7991  pncan2  7993  addsub  7997  addsub12  7999  addsubeq4  8001  sub32  8020  pnpcan2  8026  ppncan  8028  sub4  8031  negsubdi2  8045  ltadd2  8205  ltaddnegr  8211  ltaddsub2  8223  leaddsub2  8225  leltadd  8233  ltaddpos2  8239  addge02  8259  conjmulap  8513  recreclt  8682  avgle1  8984  avgle2  8985  nn0nnaddcl  9032  xaddcom  9674  fzen  9854  fzshftral  9919  flqzadd  10102  addmodidr  10177  nn0ennn  10237  ser3add  10309  bernneq2  10444  shftval2  10630  shftval4  10632  crim  10662  resqrexlemover  10814  climshft2  11107  summodclem3  11181  binom1dif  11288  isumshft  11291  arisum  11299  mertenslemi1  11336  addcos  11489  demoivreALT  11516  dvdsaddr  11573  divalgb  11658  hashdvds  11933  ioo2bl  12751  reeff1olem  12900  ptolemy  12953