Theorem addcom 8415

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130   + caddc 8135

This theorem was proved from axioms:  ax-addcom 8232

This theorem is referenced by:  addlid  8417  readdcan  8418  addcomi  8422  addcomd  8429  add12  8436  add32  8437  add42  8440  cnegexlem1  8453  cnegexlem3  8455  cnegex2  8457  subsub23  8483  pncan2  8485  addsub  8489  addsub12  8491  addsubeq4  8493  sub32  8512  pnpcan2  8518  ppncan  8520  sub4  8523  negsubdi2  8537  ltadd2  8698  ltaddnegr  8704  ltaddsub2  8716  leaddsub2  8718  leltadd  8726  ltaddpos2  8732  addge02  8752  conjmulap  9008  recreclt  9179  avgle1  9484  avgle2  9485  nn0nnaddcl  9532  xaddcom  10200  fzen  10383  fzshftral  10449  fzo0addelr  10541  flqzadd  10665  addmodidr  10742  nn0ennn  10802  ser3add  10891  bernneq2  11031  ccatrn  11305  ccatalpha  11309  shftval2  11519  shftval4  11521  crim  11551  resqrexlemover  11703  climshft2  11999  summodclem3  12074  binom1dif  12181  isumshft  12184  arisum  12192  mertenslemi1  12229  addcos  12440  demoivreALT  12468  dvdsaddr  12531  divalgb  12619  hashdvds  12926  pythagtriplem2  12972  mulgnndir  13889  cncrng  14766  ioo2bl  15465  reeff1olem  15685  ptolemy  15738  wilthlem1  15897  1sgmprm  15911  perfectlem2  15917