Theorem addcom 8321

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035   + caddc 8040

This theorem was proved from axioms:  ax-addcom 8137

This theorem is referenced by:  addlid  8323  readdcan  8324  addcomi  8328  addcomd  8335  add12  8342  add32  8343  add42  8346  cnegexlem1  8359  cnegexlem3  8361  cnegex2  8363  subsub23  8389  pncan2  8391  addsub  8395  addsub12  8397  addsubeq4  8399  sub32  8418  pnpcan2  8424  ppncan  8426  sub4  8429  negsubdi2  8443  ltadd2  8604  ltaddnegr  8610  ltaddsub2  8622  leaddsub2  8624  leltadd  8632  ltaddpos2  8638  addge02  8658  conjmulap  8914  recreclt  9085  avgle1  9390  avgle2  9391  nn0nnaddcl  9438  xaddcom  10101  fzen  10283  fzshftral  10348  fzo0addelr  10440  flqzadd  10564  addmodidr  10641  nn0ennn  10701  ser3add  10790  bernneq2  10929  ccatrn  11195  ccatalpha  11199  shftval2  11409  shftval4  11411  crim  11441  resqrexlemover  11593  climshft2  11889  summodclem3  11964  binom1dif  12071  isumshft  12074  arisum  12082  mertenslemi1  12119  addcos  12330  demoivreALT  12358  dvdsaddr  12421  divalgb  12509  hashdvds  12816  pythagtriplem2  12862  mulgnndir  13761  cncrng  14607  ioo2bl  15304  reeff1olem  15524  ptolemy  15577  wilthlem1  15733  1sgmprm  15747  perfectlem2  15753