Theorem addcom 8031

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1343   e. wcel 2136  (class class class)co 5841   CCcc 7747   + caddc 7752

This theorem was proved from axioms:  ax-addcom 7849

This theorem is referenced by:  addid2  8033  readdcan  8034  addcomi  8038  addcomd  8045  add12  8052  add32  8053  add42  8056  cnegexlem1  8069  cnegexlem3  8071  cnegex2  8073  subsub23  8099  pncan2  8101  addsub  8105  addsub12  8107  addsubeq4  8109  sub32  8128  pnpcan2  8134  ppncan  8136  sub4  8139  negsubdi2  8153  ltadd2  8313  ltaddnegr  8319  ltaddsub2  8331  leaddsub2  8333  leltadd  8341  ltaddpos2  8347  addge02  8367  conjmulap  8621  recreclt  8791  avgle1  9093  avgle2  9094  nn0nnaddcl  9141  xaddcom  9793  fzen  9974  fzshftral  10039  flqzadd  10229  addmodidr  10304  nn0ennn  10364  ser3add  10436  bernneq2  10572  shftval2  10764  shftval4  10766  crim  10796  resqrexlemover  10948  climshft2  11243  summodclem3  11317  binom1dif  11424  isumshft  11427  arisum  11435  mertenslemi1  11472  addcos  11683  demoivreALT  11710  dvdsaddr  11773  divalgb  11858  hashdvds  12149  pythagtriplem2  12194  ioo2bl  13143  reeff1olem  13292  ptolemy  13345