Theorem addcom 8035

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1343   ∈ wcel 2136  (class class class)co 5842  ℂcc 7751   + caddc 7756

This theorem was proved from axioms:  ax-addcom 7853

This theorem is referenced by:  addid2  8037  readdcan  8038  addcomi  8042  addcomd  8049  add12  8056  add32  8057  add42  8060  cnegexlem1  8073  cnegexlem3  8075  cnegex2  8077  subsub23  8103  pncan2  8105  addsub  8109  addsub12  8111  addsubeq4  8113  sub32  8132  pnpcan2  8138  ppncan  8140  sub4  8143  negsubdi2  8157  ltadd2  8317  ltaddnegr  8323  ltaddsub2  8335  leaddsub2  8337  leltadd  8345  ltaddpos2  8351  addge02  8371  conjmulap  8625  recreclt  8795  avgle1  9097  avgle2  9098  nn0nnaddcl  9145  xaddcom  9797  fzen  9978  fzshftral  10043  flqzadd  10233  addmodidr  10308  nn0ennn  10368  ser3add  10440  bernneq2  10576  shftval2  10768  shftval4  10770  crim  10800  resqrexlemover  10952  climshft2  11247  summodclem3  11321  binom1dif  11428  isumshft  11431  arisum  11439  mertenslemi1  11476  addcos  11687  demoivreALT  11714  dvdsaddr  11777  divalgb  11862  hashdvds  12153  pythagtriplem2  12198  ioo2bl  13183  reeff1olem  13332  ptolemy  13385