Theorem addcom 8316

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   + caddc 8035

This theorem was proved from axioms:  ax-addcom 8132

This theorem is referenced by:  addlid  8318  readdcan  8319  addcomi  8323  addcomd  8330  add12  8337  add32  8338  add42  8341  cnegexlem1  8354  cnegexlem3  8356  cnegex2  8358  subsub23  8384  pncan2  8386  addsub  8390  addsub12  8392  addsubeq4  8394  sub32  8413  pnpcan2  8419  ppncan  8421  sub4  8424  negsubdi2  8438  ltadd2  8599  ltaddnegr  8605  ltaddsub2  8617  leaddsub2  8619  leltadd  8627  ltaddpos2  8633  addge02  8653  conjmulap  8909  recreclt  9080  avgle1  9385  avgle2  9386  nn0nnaddcl  9433  xaddcom  10096  fzen  10278  fzshftral  10343  fzo0addelr  10435  flqzadd  10559  addmodidr  10636  nn0ennn  10696  ser3add  10785  bernneq2  10924  ccatrn  11190  ccatalpha  11194  shftval2  11391  shftval4  11393  crim  11423  resqrexlemover  11575  climshft2  11871  summodclem3  11946  binom1dif  12053  isumshft  12056  arisum  12064  mertenslemi1  12101  addcos  12312  demoivreALT  12340  dvdsaddr  12403  divalgb  12491  hashdvds  12798  pythagtriplem2  12844  mulgnndir  13743  cncrng  14589  ioo2bl  15281  reeff1olem  15501  ptolemy  15554  wilthlem1  15710  1sgmprm  15724  perfectlem2  15730