Theorem addcom 8239

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   e. wcel 2177  (class class class)co 5962   CCcc 7953   + caddc 7958

This theorem was proved from axioms:  ax-addcom 8055

This theorem is referenced by:  addlid  8241  readdcan  8242  addcomi  8246  addcomd  8253  add12  8260  add32  8261  add42  8264  cnegexlem1  8277  cnegexlem3  8279  cnegex2  8281  subsub23  8307  pncan2  8309  addsub  8313  addsub12  8315  addsubeq4  8317  sub32  8336  pnpcan2  8342  ppncan  8344  sub4  8347  negsubdi2  8361  ltadd2  8522  ltaddnegr  8528  ltaddsub2  8540  leaddsub2  8542  leltadd  8550  ltaddpos2  8556  addge02  8576  conjmulap  8832  recreclt  9003  avgle1  9308  avgle2  9309  nn0nnaddcl  9356  xaddcom  10013  fzen  10195  fzshftral  10260  fzo0addelr  10350  flqzadd  10473  addmodidr  10550  nn0ennn  10610  ser3add  10699  bernneq2  10838  ccatrn  11098  shftval2  11222  shftval4  11224  crim  11254  resqrexlemover  11406  climshft2  11702  summodclem3  11776  binom1dif  11883  isumshft  11886  arisum  11894  mertenslemi1  11931  addcos  12142  demoivreALT  12170  dvdsaddr  12233  divalgb  12321  hashdvds  12628  pythagtriplem2  12674  mulgnndir  13572  cncrng  14416  ioo2bl  15108  reeff1olem  15328  ptolemy  15381  wilthlem1  15537  1sgmprm  15551  perfectlem2  15557