Theorem addcom 8471

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8184   + caddc 8189

This proof depends on axioms:  ax-addcom 8286

This theorem is used by:  addlid  8473  readdcan  8474  addcomi  8478  addcomd  8485  add12  8492  add32  8493  add42  8496  cnegexlem1  8509  cnegexlem3  8511  cnegex2  8513  subsub23  8539  pncan2  8541  addsub  8545  addsub12  8547  addsubeq4  8549  sub32  8568  pnpcan2  8574  ppncan  8576  sub4  8579  negsubdi2  8593  ltadd2  8755  ltaddnegr  8761  ltaddsub2  8773  leaddsub2  8775  leltadd  8783  ltaddpos2  8789  addge02  8809  conjmulap  9068  recreclt  9239  avgle1  9558  avgle2  9559  nn0nnaddcl  9606  xaddcom  10281  fzen  10465  fzshftral  10533  fzo0addelr  10625  flqzadd  10755  addmodidr  10832  nn0ennn  10892  ser3add  10981  bernneq2  11121  ccatrn  11400  ccatalpha  11404  shftval2  11614  shftval4  11616  crim  11646  resqrexlemover  11799  climshft2  12098  summodclem3  12173  binom1dif  12280  isumshft  12283  arisum  12291  mertenslemi1  12328  addcos  12539  demoivreALT  12567  dvdsaddr  12630  divalgb  12718  hashdvds  13029  pythagtriplem2  13075  mulgnndir  14014  cncrng  15016  ioo2bl  15789  reeff1olem  16009  ptolemy  16063  birthdaylem2  16238  wilthlem1  16244  1sgmprm  16300  perfectlem2  16312