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  11108  shftval4  11110  crim  11140  resqrexlemover  11292  climshft2  11588  summodclem3  11662  binom1dif  11769  isumshft  11772  arisum  11780  mertenslemi1  11817  addcos  12028  demoivreALT  12056  dvdsaddr  12119  divalgb  12207  hashdvds  12514  pythagtriplem2  12560  mulgnndir  13458  cncrng  14302  ioo2bl  14994  reeff1olem  15214  ptolemy  15267  wilthlem1  15423  1sgmprm  15437  perfectlem2  15443