Theorem addcom 7245

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

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   + caddc 6984

This theorem was proved from axioms:  ax-addcom 7076

This theorem is referenced by:  addid2  7247  readdcan  7248  addcomi  7252  addcomd  7259  add12  7266  add32  7267  add42  7270  cnegexlem1  7283  cnegexlem3  7285  cnegex2  7287  subsub23  7313  pncan2  7315  addsub  7319  addsub12  7321  addsubeq4  7323  sub32  7342  pnpcan2  7348  ppncan  7350  sub4  7353  negsubdi2  7367  ltadd2  7523  ltaddnegr  7529  ltaddsub2  7541  leaddsub2  7543  leltadd  7551  ltaddpos2  7557  addge02  7577  conjmulap  7817  recreclt  7978  avgle1  8271  avgle2  8272  nn0nnaddcl  8319  fzen  9062  fzshftral  9125  flqzadd  9300  addmodidr  9375  nn0ennn  9425  iseradd  9463  bernneq2  9594  shftval2  9714  shftval4  9716  crim  9745  resqrexlemover  9896  climshft2  10145  dvdsaddr  10239  divalgb  10325