Theorem addcom 8306

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 8122	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 6013   CCcc 8020   + caddc 8025

This theorem was proved from axioms:  ax-addcom 8122

This theorem is referenced by:  addlid  8308  readdcan  8309  addcomi  8313  addcomd  8320  add12  8327  add32  8328  add42  8331  cnegexlem1  8344  cnegexlem3  8346  cnegex2  8348  subsub23  8374  pncan2  8376  addsub  8380  addsub12  8382  addsubeq4  8384  sub32  8403  pnpcan2  8409  ppncan  8411  sub4  8414  negsubdi2  8428  ltadd2  8589  ltaddnegr  8595  ltaddsub2  8607  leaddsub2  8609  leltadd  8617  ltaddpos2  8623  addge02  8643  conjmulap  8899  recreclt  9070  avgle1  9375  avgle2  9376  nn0nnaddcl  9423  xaddcom  10086  fzen  10268  fzshftral  10333  fzo0addelr  10424  flqzadd  10548  addmodidr  10625  nn0ennn  10685  ser3add  10774  bernneq2  10913  ccatrn  11176  ccatalpha  11180  shftval2  11377  shftval4  11379  crim  11409  resqrexlemover  11561  climshft2  11857  summodclem3  11931  binom1dif  12038  isumshft  12041  arisum  12049  mertenslemi1  12086  addcos  12297  demoivreALT  12325  dvdsaddr  12388  divalgb  12476  hashdvds  12783  pythagtriplem2  12829  mulgnndir  13728  cncrng  14573  ioo2bl  15265  reeff1olem  15485  ptolemy  15538  wilthlem1  15694  1sgmprm  15708  perfectlem2  15714