Theorem addcom 8464

Description: Addition is commutative. (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 8279	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8177   + caddc 8182

This proof depends on axioms:  ax-addcom 8279

This theorem is used by:  addlid  8466  readdcan  8467  addcomi  8471  addcomd  8478  add12  8485  add32  8486  add42  8489  cnegexlem1  8502  cnegexlem3  8504  cnegex2  8506  subsub23  8532  pncan2  8534  addsub  8538  addsub12  8540  addsubeq4  8542  sub32  8561  pnpcan2  8567  ppncan  8569  sub4  8572  negsubdi2  8586  ltadd2  8748  ltaddnegr  8754  ltaddsub2  8766  leaddsub2  8768  leltadd  8776  ltaddpos2  8782  addge02  8802  conjmulap  9061  recreclt  9232  avgle1  9550  avgle2  9551  nn0nnaddcl  9598  xaddcom  10273  fzen  10457  fzshftral  10525  fzo0addelr  10617  flqzadd  10746  addmodidr  10823  nn0ennn  10883  ser3add  10972  bernneq2  11112  ccatrn  11391  ccatalpha  11395  shftval2  11605  shftval4  11607  crim  11637  resqrexlemover  11790  climshft2  12088  summodclem3  12163  binom1dif  12270  isumshft  12273  arisum  12281  mertenslemi1  12318  addcos  12529  demoivreALT  12557  dvdsaddr  12620  divalgb  12708  hashdvds  13019  pythagtriplem2  13065  mulgnndir  14003  cncrng  14955  ioo2bl  15701  reeff1olem  15921  ptolemy  15975  birthdaylem2  16145  wilthlem1  16151  1sgmprm  16189  perfectlem2  16198