Theorem addcom 8182

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901

This theorem was proved from axioms:  ax-addcom 7998

This theorem is referenced by:  addlid  8184  readdcan  8185  addcomi  8189  addcomd  8196  add12  8203  add32  8204  add42  8207  cnegexlem1  8220  cnegexlem3  8222  cnegex2  8224  subsub23  8250  pncan2  8252  addsub  8256  addsub12  8258  addsubeq4  8260  sub32  8279  pnpcan2  8285  ppncan  8287  sub4  8290  negsubdi2  8304  ltadd2  8465  ltaddnegr  8471  ltaddsub2  8483  leaddsub2  8485  leltadd  8493  ltaddpos2  8499  addge02  8519  conjmulap  8775  recreclt  8946  avgle1  9251  avgle2  9252  nn0nnaddcl  9299  xaddcom  9955  fzen  10137  fzshftral  10202  flqzadd  10407  addmodidr  10484  nn0ennn  10544  ser3add  10633  bernneq2  10772  shftval2  11010  shftval4  11012  crim  11042  resqrexlemover  11194  climshft2  11490  summodclem3  11564  binom1dif  11671  isumshft  11674  arisum  11682  mertenslemi1  11719  addcos  11930  demoivreALT  11958  dvdsaddr  12021  divalgb  12109  hashdvds  12416  pythagtriplem2  12462  mulgnndir  13359  cncrng  14203  ioo2bl  14873  reeff1olem  15093  ptolemy  15146  wilthlem1  15302  1sgmprm  15316  perfectlem2  15322