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  10280  fzen  10464  fzshftral  10532  fzo0addelr  10624  flqzadd  10754  addmodidr  10831  nn0ennn  10891  ser3add  10980  bernneq2  11120  ccatrn  11399  ccatalpha  11403  shftval2  11613  shftval4  11615  crim  11645  resqrexlemover  11798  climshft2  12097  summodclem3  12172  binom1dif  12279  isumshft  12282  arisum  12290  mertenslemi1  12327  addcos  12538  demoivreALT  12566  dvdsaddr  12629  divalgb  12717  hashdvds  13028  pythagtriplem2  13074  mulgnndir  14013  cncrng  15015  ioo2bl  15777  reeff1olem  15997  ptolemy  16051  birthdaylem2  16226  wilthlem1  16232  1sgmprm  16288  perfectlem2  16300