Theorem addcom 8279

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   e. wcel 2200  (class class class)co 6000   CCcc 7993   + caddc 7998

This theorem was proved from axioms:  ax-addcom 8095

This theorem is referenced by:  addlid  8281  readdcan  8282  addcomi  8286  addcomd  8293  add12  8300  add32  8301  add42  8304  cnegexlem1  8317  cnegexlem3  8319  cnegex2  8321  subsub23  8347  pncan2  8349  addsub  8353  addsub12  8355  addsubeq4  8357  sub32  8376  pnpcan2  8382  ppncan  8384  sub4  8387  negsubdi2  8401  ltadd2  8562  ltaddnegr  8568  ltaddsub2  8580  leaddsub2  8582  leltadd  8590  ltaddpos2  8596  addge02  8616  conjmulap  8872  recreclt  9043  avgle1  9348  avgle2  9349  nn0nnaddcl  9396  xaddcom  10053  fzen  10235  fzshftral  10300  fzo0addelr  10390  flqzadd  10513  addmodidr  10590  nn0ennn  10650  ser3add  10739  bernneq2  10878  ccatrn  11139  shftval2  11332  shftval4  11334  crim  11364  resqrexlemover  11516  climshft2  11812  summodclem3  11886  binom1dif  11993  isumshft  11996  arisum  12004  mertenslemi1  12041  addcos  12252  demoivreALT  12280  dvdsaddr  12343  divalgb  12431  hashdvds  12738  pythagtriplem2  12784  mulgnndir  13683  cncrng  14527  ioo2bl  15219  reeff1olem  15439  ptolemy  15492  wilthlem1  15648  1sgmprm  15662  perfectlem2  15668