Theorem addcom 8208

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1372   e. wcel 2175  (class class class)co 5943   CCcc 7922   + caddc 7927

This theorem was proved from axioms:  ax-addcom 8024

This theorem is referenced by:  addlid  8210  readdcan  8211  addcomi  8215  addcomd  8222  add12  8229  add32  8230  add42  8233  cnegexlem1  8246  cnegexlem3  8248  cnegex2  8250  subsub23  8276  pncan2  8278  addsub  8282  addsub12  8284  addsubeq4  8286  sub32  8305  pnpcan2  8311  ppncan  8313  sub4  8316  negsubdi2  8330  ltadd2  8491  ltaddnegr  8497  ltaddsub2  8509  leaddsub2  8511  leltadd  8519  ltaddpos2  8525  addge02  8545  conjmulap  8801  recreclt  8972  avgle1  9277  avgle2  9278  nn0nnaddcl  9325  xaddcom  9982  fzen  10164  fzshftral  10229  fzo0addelr  10316  flqzadd  10439  addmodidr  10516  nn0ennn  10576  ser3add  10665  bernneq2  10804  ccatrn  11063  shftval2  11079  shftval4  11081  crim  11111  resqrexlemover  11263  climshft2  11559  summodclem3  11633  binom1dif  11740  isumshft  11743  arisum  11751  mertenslemi1  11788  addcos  11999  demoivreALT  12027  dvdsaddr  12090  divalgb  12178  hashdvds  12485  pythagtriplem2  12531  mulgnndir  13429  cncrng  14273  ioo2bl  14965  reeff1olem  15185  ptolemy  15238  wilthlem1  15394  1sgmprm  15408  perfectlem2  15414