Theorem addcom 8463

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 8279	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 8177   + caddc 8182

This proof depends on axioms:  ax-addcom 8279

This theorem is used by:  addlid  8465  readdcan  8466  addcomi  8470  addcomd  8477  add12  8484  add32  8485  add42  8488  cnegexlem1  8501  cnegexlem3  8503  cnegex2  8505  subsub23  8531  pncan2  8533  addsub  8537  addsub12  8539  addsubeq4  8541  sub32  8560  pnpcan2  8566  ppncan  8568  sub4  8571  negsubdi2  8585  ltadd2  8747  ltaddnegr  8753  ltaddsub2  8765  leaddsub2  8767  leltadd  8775  ltaddpos2  8781  addge02  8801  conjmulap  9059  recreclt  9230  avgle1  9546  avgle2  9547  nn0nnaddcl  9594  xaddcom  10263  fzen  10447  fzshftral  10515  fzo0addelr  10607  flqzadd  10733  addmodidr  10810  nn0ennn  10870  ser3add  10959  bernneq2  11099  ccatrn  11377  ccatalpha  11381  shftval2  11591  shftval4  11593  crim  11623  resqrexlemover  11776  climshft2  12072  summodclem3  12147  binom1dif  12254  isumshft  12257  arisum  12265  mertenslemi1  12302  addcos  12513  demoivreALT  12541  dvdsaddr  12604  divalgb  12692  hashdvds  12999  pythagtriplem2  13045  mulgnndir  13954  cncrng  14906  ioo2bl  15652  reeff1olem  15872  ptolemy  15925  birthdaylem2  16088  wilthlem1  16094  1sgmprm  16108  perfectlem2  16114