Theorem addcom 8294

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   e. wcel 2200  (class class class)co 6007   CCcc 8008   + caddc 8013

This theorem was proved from axioms:  ax-addcom 8110

This theorem is referenced by:  addlid  8296  readdcan  8297  addcomi  8301  addcomd  8308  add12  8315  add32  8316  add42  8319  cnegexlem1  8332  cnegexlem3  8334  cnegex2  8336  subsub23  8362  pncan2  8364  addsub  8368  addsub12  8370  addsubeq4  8372  sub32  8391  pnpcan2  8397  ppncan  8399  sub4  8402  negsubdi2  8416  ltadd2  8577  ltaddnegr  8583  ltaddsub2  8595  leaddsub2  8597  leltadd  8605  ltaddpos2  8611  addge02  8631  conjmulap  8887  recreclt  9058  avgle1  9363  avgle2  9364  nn0nnaddcl  9411  xaddcom  10069  fzen  10251  fzshftral  10316  fzo0addelr  10407  flqzadd  10530  addmodidr  10607  nn0ennn  10667  ser3add  10756  bernneq2  10895  ccatrn  11157  ccatalpha  11161  shftval2  11352  shftval4  11354  crim  11384  resqrexlemover  11536  climshft2  11832  summodclem3  11906  binom1dif  12013  isumshft  12016  arisum  12024  mertenslemi1  12061  addcos  12272  demoivreALT  12300  dvdsaddr  12363  divalgb  12451  hashdvds  12758  pythagtriplem2  12804  mulgnndir  13703  cncrng  14548  ioo2bl  15240  reeff1olem  15460  ptolemy  15513  wilthlem1  15669  1sgmprm  15683  perfectlem2  15689