Theorem addcom 8096

Description: Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)

Assertion

Ref	Expression
addcom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcom

Step	Hyp	Ref	Expression
1		ax-addcom 7913	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353   ∈ wcel 2148  (class class class)co 5877  ℂcc 7811   + caddc 7816

This theorem was proved from axioms:  ax-addcom 7913

This theorem is referenced by:  addlid  8098  readdcan  8099  addcomi  8103  addcomd  8110  add12  8117  add32  8118  add42  8121  cnegexlem1  8134  cnegexlem3  8136  cnegex2  8138  subsub23  8164  pncan2  8166  addsub  8170  addsub12  8172  addsubeq4  8174  sub32  8193  pnpcan2  8199  ppncan  8201  sub4  8204  negsubdi2  8218  ltadd2  8378  ltaddnegr  8384  ltaddsub2  8396  leaddsub2  8398  leltadd  8406  ltaddpos2  8412  addge02  8432  conjmulap  8688  recreclt  8859  avgle1  9161  avgle2  9162  nn0nnaddcl  9209  xaddcom  9863  fzen  10045  fzshftral  10110  flqzadd  10300  addmodidr  10375  nn0ennn  10435  ser3add  10507  bernneq2  10644  shftval2  10837  shftval4  10839  crim  10869  resqrexlemover  11021  climshft2  11316  summodclem3  11390  binom1dif  11497  isumshft  11500  arisum  11508  mertenslemi1  11545  addcos  11756  demoivreALT  11783  dvdsaddr  11846  divalgb  11932  hashdvds  12223  pythagtriplem2  12268  mulgnndir  13017  cncrng  13548  ioo2bl  14128  reeff1olem  14277  ptolemy  14330