Theorem addcom 8246

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   e. wcel 2178  (class class class)co 5969   CCcc 7960   + caddc 7965

This theorem was proved from axioms:  ax-addcom 8062

This theorem is referenced by:  addlid  8248  readdcan  8249  addcomi  8253  addcomd  8260  add12  8267  add32  8268  add42  8271  cnegexlem1  8284  cnegexlem3  8286  cnegex2  8288  subsub23  8314  pncan2  8316  addsub  8320  addsub12  8322  addsubeq4  8324  sub32  8343  pnpcan2  8349  ppncan  8351  sub4  8354  negsubdi2  8368  ltadd2  8529  ltaddnegr  8535  ltaddsub2  8547  leaddsub2  8549  leltadd  8557  ltaddpos2  8563  addge02  8583  conjmulap  8839  recreclt  9010  avgle1  9315  avgle2  9316  nn0nnaddcl  9363  xaddcom  10020  fzen  10202  fzshftral  10267  fzo0addelr  10357  flqzadd  10480  addmodidr  10557  nn0ennn  10617  ser3add  10706  bernneq2  10845  ccatrn  11105  shftval2  11298  shftval4  11300  crim  11330  resqrexlemover  11482  climshft2  11778  summodclem3  11852  binom1dif  11959  isumshft  11962  arisum  11970  mertenslemi1  12007  addcos  12218  demoivreALT  12246  dvdsaddr  12309  divalgb  12397  hashdvds  12704  pythagtriplem2  12750  mulgnndir  13648  cncrng  14492  ioo2bl  15184  reeff1olem  15404  ptolemy  15457  wilthlem1  15613  1sgmprm  15627  perfectlem2  15633