Theorem addcom 8465

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   + caddc 8183

This proof depends on axioms:  ax-addcom 8280

This theorem is used by:  addlid  8467  readdcan  8468  addcomi  8472  addcomd  8479  add12  8486  add32  8487  add42  8490  cnegexlem1  8503  cnegexlem3  8505  cnegex2  8507  subsub23  8533  pncan2  8535  addsub  8539  addsub12  8541  addsubeq4  8543  sub32  8562  pnpcan2  8568  ppncan  8570  sub4  8573  negsubdi2  8587  ltadd2  8749  ltaddnegr  8755  ltaddsub2  8767  leaddsub2  8769  leltadd  8777  ltaddpos2  8783  addge02  8803  conjmulap  9062  recreclt  9233  avgle1  9551  avgle2  9552  nn0nnaddcl  9599  xaddcom  10274  fzen  10458  fzshftral  10526  fzo0addelr  10618  flqzadd  10748  addmodidr  10825  nn0ennn  10885  ser3add  10974  bernneq2  11114  ccatrn  11393  ccatalpha  11397  shftval2  11607  shftval4  11609  crim  11639  resqrexlemover  11792  climshft2  12091  summodclem3  12166  binom1dif  12273  isumshft  12276  arisum  12284  mertenslemi1  12321  addcos  12532  demoivreALT  12560  dvdsaddr  12623  divalgb  12711  hashdvds  13022  pythagtriplem2  13068  mulgnndir  14007  cncrng  14990  ioo2bl  15743  reeff1olem  15963  ptolemy  16017  birthdaylem2  16187  wilthlem1  16193  1sgmprm  16249  perfectlem2  16261