Theorem addcom 8410

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2203  (class class class)co 6050   CCcc 8125   + caddc 8130

This theorem was proved from axioms:  ax-addcom 8227

This theorem is referenced by:  addlid  8412  readdcan  8413  addcomi  8417  addcomd  8424  add12  8431  add32  8432  add42  8435  cnegexlem1  8448  cnegexlem3  8450  cnegex2  8452  subsub23  8478  pncan2  8480  addsub  8484  addsub12  8486  addsubeq4  8488  sub32  8507  pnpcan2  8513  ppncan  8515  sub4  8518  negsubdi2  8532  ltadd2  8693  ltaddnegr  8699  ltaddsub2  8711  leaddsub2  8713  leltadd  8721  ltaddpos2  8727  addge02  8747  conjmulap  9003  recreclt  9174  avgle1  9479  avgle2  9480  nn0nnaddcl  9527  xaddcom  10194  fzen  10377  fzshftral  10442  fzo0addelr  10534  flqzadd  10658  addmodidr  10735  nn0ennn  10795  ser3add  10884  bernneq2  11023  ccatrn  11297  ccatalpha  11301  shftval2  11511  shftval4  11513  crim  11543  resqrexlemover  11695  climshft2  11991  summodclem3  12066  binom1dif  12173  isumshft  12176  arisum  12184  mertenslemi1  12221  addcos  12432  demoivreALT  12460  dvdsaddr  12523  divalgb  12611  hashdvds  12918  pythagtriplem2  12964  mulgnndir  13868  cncrng  14717  ioo2bl  15416  reeff1olem  15636  ptolemy  15689  wilthlem1  15848  1sgmprm  15862  perfectlem2  15868