Theorem addcom 8180

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   e. wcel 2167  (class class class)co 5925   CCcc 7894   + caddc 7899

This theorem was proved from axioms:  ax-addcom 7996

This theorem is referenced by:  addlid  8182  readdcan  8183  addcomi  8187  addcomd  8194  add12  8201  add32  8202  add42  8205  cnegexlem1  8218  cnegexlem3  8220  cnegex2  8222  subsub23  8248  pncan2  8250  addsub  8254  addsub12  8256  addsubeq4  8258  sub32  8277  pnpcan2  8283  ppncan  8285  sub4  8288  negsubdi2  8302  ltadd2  8463  ltaddnegr  8469  ltaddsub2  8481  leaddsub2  8483  leltadd  8491  ltaddpos2  8497  addge02  8517  conjmulap  8773  recreclt  8944  avgle1  9249  avgle2  9250  nn0nnaddcl  9297  xaddcom  9953  fzen  10135  fzshftral  10200  flqzadd  10405  addmodidr  10482  nn0ennn  10542  ser3add  10631  bernneq2  10770  shftval2  11008  shftval4  11010  crim  11040  resqrexlemover  11192  climshft2  11488  summodclem3  11562  binom1dif  11669  isumshft  11672  arisum  11680  mertenslemi1  11717  addcos  11928  demoivreALT  11956  dvdsaddr  12019  divalgb  12107  hashdvds  12414  pythagtriplem2  12460  mulgnndir  13357  cncrng  14201  ioo2bl  14871  reeff1olem  15091  ptolemy  15144  wilthlem1  15300  1sgmprm  15314  perfectlem2  15320