Theorem addcom 7617

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

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1289   e. wcel 1438  (class class class)co 5652   CCcc 7346   + caddc 7351

This theorem was proved from axioms:  ax-addcom 7443

This theorem is referenced by:  addid2  7619  readdcan  7620  addcomi  7624  addcomd  7631  add12  7638  add32  7639  add42  7642  cnegexlem1  7655  cnegexlem3  7657  cnegex2  7659  subsub23  7685  pncan2  7687  addsub  7691  addsub12  7693  addsubeq4  7695  sub32  7714  pnpcan2  7720  ppncan  7722  sub4  7725  negsubdi2  7739  ltadd2  7895  ltaddnegr  7901  ltaddsub2  7913  leaddsub2  7915  leltadd  7923  ltaddpos2  7929  addge02  7949  conjmulap  8194  recreclt  8359  avgle1  8654  avgle2  8655  nn0nnaddcl  8702  fzen  9455  fzshftral  9518  flqzadd  9701  addmodidr  9776  nn0ennn  9836  iseradd  9930  bernneq2  10071  shftval2  10256  shftval4  10258  crim  10288  resqrexlemover  10439  climshft2  10691  isummolem3  10766  binom1dif  10877  isumshft  10880  arisum  10888  mertenslemi1  10925  addcos  11033  demoivreALT  11059  dvdsaddr  11114  divalgb  11199  hashdvds  11471