Theorem addcom 7892

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1331   e. wcel 1480  (class class class)co 5767   CCcc 7611   + caddc 7616

This theorem was proved from axioms:  ax-addcom 7713

This theorem is referenced by:  addid2  7894  readdcan  7895  addcomi  7899  addcomd  7906  add12  7913  add32  7914  add42  7917  cnegexlem1  7930  cnegexlem3  7932  cnegex2  7934  subsub23  7960  pncan2  7962  addsub  7966  addsub12  7968  addsubeq4  7970  sub32  7989  pnpcan2  7995  ppncan  7997  sub4  8000  negsubdi2  8014  ltadd2  8174  ltaddnegr  8180  ltaddsub2  8192  leaddsub2  8194  leltadd  8202  ltaddpos2  8208  addge02  8228  conjmulap  8482  recreclt  8651  avgle1  8953  avgle2  8954  nn0nnaddcl  9001  xaddcom  9637  fzen  9816  fzshftral  9881  flqzadd  10064  addmodidr  10139  nn0ennn  10199  ser3add  10271  bernneq2  10406  shftval2  10591  shftval4  10593  crim  10623  resqrexlemover  10775  climshft2  11068  summodclem3  11142  binom1dif  11249  isumshft  11252  arisum  11260  mertenslemi1  11297  addcos  11442  demoivreALT  11469  dvdsaddr  11526  divalgb  11611  hashdvds  11886  ioo2bl  12701  ptolemy  12894