Theorem addcom 8158

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   + caddc 7877

This theorem was proved from axioms:  ax-addcom 7974

This theorem is referenced by:  addlid  8160  readdcan  8161  addcomi  8165  addcomd  8172  add12  8179  add32  8180  add42  8183  cnegexlem1  8196  cnegexlem3  8198  cnegex2  8200  subsub23  8226  pncan2  8228  addsub  8232  addsub12  8234  addsubeq4  8236  sub32  8255  pnpcan2  8261  ppncan  8263  sub4  8266  negsubdi2  8280  ltadd2  8440  ltaddnegr  8446  ltaddsub2  8458  leaddsub2  8460  leltadd  8468  ltaddpos2  8474  addge02  8494  conjmulap  8750  recreclt  8921  avgle1  9226  avgle2  9227  nn0nnaddcl  9274  xaddcom  9930  fzen  10112  fzshftral  10177  flqzadd  10370  addmodidr  10447  nn0ennn  10507  ser3add  10596  bernneq2  10735  shftval2  10973  shftval4  10975  crim  11005  resqrexlemover  11157  climshft2  11452  summodclem3  11526  binom1dif  11633  isumshft  11636  arisum  11644  mertenslemi1  11681  addcos  11892  demoivreALT  11920  dvdsaddr  11983  divalgb  12069  hashdvds  12362  pythagtriplem2  12407  mulgnndir  13224  cncrng  14068  ioo2bl  14730  reeff1olem  14947  ptolemy  15000  wilthlem1  15153