Theorem addcom 8163

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 7979	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 5922   CCcc 7877   + caddc 7882

This theorem was proved from axioms:  ax-addcom 7979

This theorem is referenced by:  addlid  8165  readdcan  8166  addcomi  8170  addcomd  8177  add12  8184  add32  8185  add42  8188  cnegexlem1  8201  cnegexlem3  8203  cnegex2  8205  subsub23  8231  pncan2  8233  addsub  8237  addsub12  8239  addsubeq4  8241  sub32  8260  pnpcan2  8266  ppncan  8268  sub4  8271  negsubdi2  8285  ltadd2  8446  ltaddnegr  8452  ltaddsub2  8464  leaddsub2  8466  leltadd  8474  ltaddpos2  8480  addge02  8500  conjmulap  8756  recreclt  8927  avgle1  9232  avgle2  9233  nn0nnaddcl  9280  xaddcom  9936  fzen  10118  fzshftral  10183  flqzadd  10388  addmodidr  10465  nn0ennn  10525  ser3add  10614  bernneq2  10753  shftval2  10991  shftval4  10993  crim  11023  resqrexlemover  11175  climshft2  11471  summodclem3  11545  binom1dif  11652  isumshft  11655  arisum  11663  mertenslemi1  11700  addcos  11911  demoivreALT  11939  dvdsaddr  12002  divalgb  12090  hashdvds  12389  pythagtriplem2  12435  mulgnndir  13281  cncrng  14125  ioo2bl  14787  reeff1olem  15007  ptolemy  15060  wilthlem1  15216  1sgmprm  15230  perfectlem2  15236