Theorem addcom 8216

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930   + caddc 7935

This theorem was proved from axioms:  ax-addcom 8032

This theorem is referenced by:  addlid  8218  readdcan  8219  addcomi  8223  addcomd  8230  add12  8237  add32  8238  add42  8241  cnegexlem1  8254  cnegexlem3  8256  cnegex2  8258  subsub23  8284  pncan2  8286  addsub  8290  addsub12  8292  addsubeq4  8294  sub32  8313  pnpcan2  8319  ppncan  8321  sub4  8324  negsubdi2  8338  ltadd2  8499  ltaddnegr  8505  ltaddsub2  8517  leaddsub2  8519  leltadd  8527  ltaddpos2  8533  addge02  8553  conjmulap  8809  recreclt  8980  avgle1  9285  avgle2  9286  nn0nnaddcl  9333  xaddcom  9990  fzen  10172  fzshftral  10237  fzo0addelr  10325  flqzadd  10448  addmodidr  10525  nn0ennn  10585  ser3add  10674  bernneq2  10813  ccatrn  11073  shftval2  11181  shftval4  11183  crim  11213  resqrexlemover  11365  climshft2  11661  summodclem3  11735  binom1dif  11842  isumshft  11845  arisum  11853  mertenslemi1  11890  addcos  12101  demoivreALT  12129  dvdsaddr  12192  divalgb  12280  hashdvds  12587  pythagtriplem2  12633  mulgnndir  13531  cncrng  14375  ioo2bl  15067  reeff1olem  15287  ptolemy  15340  wilthlem1  15496  1sgmprm  15510  perfectlem2  15516