Theorem addcom 8453

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209  (class class class)co 6075   CCcc 8167   + caddc 8172

This theorem was proved from axioms:  ax-addcom 8269

This theorem is referenced by:  addlid  8455  readdcan  8456  addcomi  8460  addcomd  8467  add12  8474  add32  8475  add42  8478  cnegexlem1  8491  cnegexlem3  8493  cnegex2  8495  subsub23  8521  pncan2  8523  addsub  8527  addsub12  8529  addsubeq4  8531  sub32  8550  pnpcan2  8556  ppncan  8558  sub4  8561  negsubdi2  8575  ltadd2  8737  ltaddnegr  8743  ltaddsub2  8755  leaddsub2  8757  leltadd  8765  ltaddpos2  8771  addge02  8791  conjmulap  9049  recreclt  9220  avgle1  9525  avgle2  9526  nn0nnaddcl  9573  xaddcom  10242  fzen  10426  fzshftral  10493  fzo0addelr  10585  flqzadd  10711  addmodidr  10788  nn0ennn  10848  ser3add  10937  bernneq2  11077  ccatrn  11355  ccatalpha  11359  shftval2  11569  shftval4  11571  crim  11601  resqrexlemover  11754  climshft2  12050  summodclem3  12125  binom1dif  12232  isumshft  12235  arisum  12243  mertenslemi1  12280  addcos  12491  demoivreALT  12519  dvdsaddr  12582  divalgb  12670  hashdvds  12977  pythagtriplem2  13023  mulgnndir  13931  cncrng  14878  ioo2bl  15575  reeff1olem  15795  ptolemy  15848  wilthlem1  16008  1sgmprm  16022  perfectlem2  16028