Theorem addcom 8093

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 7910	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353   ∈ wcel 2148  (class class class)co 5874  ℂcc 7808   + caddc 7813

This theorem was proved from axioms:  ax-addcom 7910

This theorem is referenced by:  addlid  8095  readdcan  8096  addcomi  8100  addcomd  8107  add12  8114  add32  8115  add42  8118  cnegexlem1  8131  cnegexlem3  8133  cnegex2  8135  subsub23  8161  pncan2  8163  addsub  8167  addsub12  8169  addsubeq4  8171  sub32  8190  pnpcan2  8196  ppncan  8198  sub4  8201  negsubdi2  8215  ltadd2  8375  ltaddnegr  8381  ltaddsub2  8393  leaddsub2  8395  leltadd  8403  ltaddpos2  8409  addge02  8429  conjmulap  8685  recreclt  8856  avgle1  9158  avgle2  9159  nn0nnaddcl  9206  xaddcom  9860  fzen  10042  fzshftral  10107  flqzadd  10297  addmodidr  10372  nn0ennn  10432  ser3add  10504  bernneq2  10641  shftval2  10834  shftval4  10836  crim  10866  resqrexlemover  11018  climshft2  11313  summodclem3  11387  binom1dif  11494  isumshft  11497  arisum  11505  mertenslemi1  11542  addcos  11753  demoivreALT  11780  dvdsaddr  11843  divalgb  11929  hashdvds  12220  pythagtriplem2  12265  mulgnndir  13010  cncrng  13433  ioo2bl  14013  reeff1olem  14162  ptolemy  14215