Theorem addcom 8358

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2202  (class class class)co 6028   CCcc 8073   + caddc 8078

This theorem was proved from axioms:  ax-addcom 8175

This theorem is referenced by:  addlid  8360  readdcan  8361  addcomi  8365  addcomd  8372  add12  8379  add32  8380  add42  8383  cnegexlem1  8396  cnegexlem3  8398  cnegex2  8400  subsub23  8426  pncan2  8428  addsub  8432  addsub12  8434  addsubeq4  8436  sub32  8455  pnpcan2  8461  ppncan  8463  sub4  8466  negsubdi2  8480  ltadd2  8641  ltaddnegr  8647  ltaddsub2  8659  leaddsub2  8661  leltadd  8669  ltaddpos2  8675  addge02  8695  conjmulap  8951  recreclt  9122  avgle1  9427  avgle2  9428  nn0nnaddcl  9475  xaddcom  10140  fzen  10323  fzshftral  10388  fzo0addelr  10480  flqzadd  10604  addmodidr  10681  nn0ennn  10741  ser3add  10830  bernneq2  10969  ccatrn  11235  ccatalpha  11239  shftval2  11449  shftval4  11451  crim  11481  resqrexlemover  11633  climshft2  11929  summodclem3  12004  binom1dif  12111  isumshft  12114  arisum  12122  mertenslemi1  12159  addcos  12370  demoivreALT  12398  dvdsaddr  12461  divalgb  12549  hashdvds  12856  pythagtriplem2  12902  mulgnndir  13801  cncrng  14648  ioo2bl  15345  reeff1olem  15565  ptolemy  15618  wilthlem1  15777  1sgmprm  15791  perfectlem2  15797