Theorem addcom 8470

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 8285	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 6088   CCcc 8183   + caddc 8188

This proof depends on axioms:  ax-addcom 8285

This theorem is used by:  addlid  8472  readdcan  8473  addcomi  8477  addcomd  8484  add12  8491  add32  8492  add42  8495  cnegexlem1  8508  cnegexlem3  8510  cnegex2  8512  subsub23  8538  pncan2  8540  addsub  8544  addsub12  8546  addsubeq4  8548  sub32  8567  pnpcan2  8573  ppncan  8575  sub4  8578  negsubdi2  8592  ltadd2  8754  ltaddnegr  8760  ltaddsub2  8772  leaddsub2  8774  leltadd  8782  ltaddpos2  8788  addge02  8808  conjmulap  9067  recreclt  9238  avgle1  9557  avgle2  9558  nn0nnaddcl  9605  xaddcom  10279  fzen  10463  fzshftral  10531  fzo0addelr  10623  flqzadd  10753  addmodidr  10830  nn0ennn  10890  ser3add  10979  bernneq2  11119  ccatrn  11398  ccatalpha  11402  shftval2  11612  shftval4  11614  crim  11644  resqrexlemover  11797  climshft2  12096  summodclem3  12171  binom1dif  12278  isumshft  12281  arisum  12289  mertenslemi1  12326  addcos  12537  demoivreALT  12565  dvdsaddr  12628  divalgb  12716  hashdvds  13027  pythagtriplem2  13073  mulgnndir  14012  cncrng  15014  ioo2bl  15794  reeff1olem  16014  ptolemy  16068  birthdaylem2  16243  wilthlem1  16249  1sgmprm  16305  perfectlem2  16317