Theorem addcom 8426

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   + caddc 8146

This theorem was proved from axioms:  ax-addcom 8243

This theorem is referenced by:  addlid  8428  readdcan  8429  addcomi  8433  addcomd  8440  add12  8447  add32  8448  add42  8451  cnegexlem1  8464  cnegexlem3  8466  cnegex2  8468  subsub23  8494  pncan2  8496  addsub  8500  addsub12  8502  addsubeq4  8504  sub32  8523  pnpcan2  8529  ppncan  8531  sub4  8534  negsubdi2  8548  ltadd2  8710  ltaddnegr  8716  ltaddsub2  8728  leaddsub2  8730  leltadd  8738  ltaddpos2  8744  addge02  8764  conjmulap  9020  recreclt  9191  avgle1  9496  avgle2  9497  nn0nnaddcl  9544  xaddcom  10213  fzen  10397  fzshftral  10464  fzo0addelr  10556  flqzadd  10682  addmodidr  10759  nn0ennn  10819  ser3add  10908  bernneq2  11048  ccatrn  11322  ccatalpha  11326  shftval2  11536  shftval4  11538  crim  11568  resqrexlemover  11720  climshft2  12016  summodclem3  12091  binom1dif  12198  isumshft  12201  arisum  12209  mertenslemi1  12246  addcos  12457  demoivreALT  12485  dvdsaddr  12548  divalgb  12636  hashdvds  12943  pythagtriplem2  12989  mulgnndir  13904  cncrng  14843  ioo2bl  15542  reeff1olem  15762  ptolemy  15815  wilthlem1  15974  1sgmprm  15988  perfectlem2  15994