Theorem addcom 8457

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

Assertion

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

Proof of Theorem addcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   + caddc 8176

This theorem was proved from axioms:  ax-addcom 8273

This theorem is referenced by:  addlid  8459  readdcan  8460  addcomi  8464  addcomd  8471  add12  8478  add32  8479  add42  8482  cnegexlem1  8495  cnegexlem3  8497  cnegex2  8499  subsub23  8525  pncan2  8527  addsub  8531  addsub12  8533  addsubeq4  8535  sub32  8554  pnpcan2  8560  ppncan  8562  sub4  8565  negsubdi2  8579  ltadd2  8741  ltaddnegr  8747  ltaddsub2  8759  leaddsub2  8761  leltadd  8769  ltaddpos2  8775  addge02  8795  conjmulap  9053  recreclt  9224  avgle1  9529  avgle2  9530  nn0nnaddcl  9577  xaddcom  10246  fzen  10430  fzshftral  10498  fzo0addelr  10590  flqzadd  10716  addmodidr  10793  nn0ennn  10853  ser3add  10942  bernneq2  11082  ccatrn  11360  ccatalpha  11364  shftval2  11574  shftval4  11576  crim  11606  resqrexlemover  11759  climshft2  12055  summodclem3  12130  binom1dif  12237  isumshft  12240  arisum  12248  mertenslemi1  12285  addcos  12496  demoivreALT  12524  dvdsaddr  12587  divalgb  12675  hashdvds  12982  pythagtriplem2  13028  mulgnndir  13937  cncrng  14889  ioo2bl  15635  reeff1olem  15855  ptolemy  15908  birthdaylem2  16071  wilthlem1  16077  1sgmprm  16091  perfectlem2  16097