Theorem addcom 8427

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   + caddc 8146

This theorem was proved from axioms:  ax-addcom 8243

This theorem is referenced by:  addlid  8429  readdcan  8430  addcomi  8434  addcomd  8441  add12  8448  add32  8449  add42  8452  cnegexlem1  8465  cnegexlem3  8467  cnegex2  8469  subsub23  8495  pncan2  8497  addsub  8501  addsub12  8503  addsubeq4  8505  sub32  8524  pnpcan2  8530  ppncan  8532  sub4  8535  negsubdi2  8549  ltadd2  8711  ltaddnegr  8717  ltaddsub2  8729  leaddsub2  8731  leltadd  8739  ltaddpos2  8745  addge02  8765  conjmulap  9023  recreclt  9194  avgle1  9499  avgle2  9500  nn0nnaddcl  9547  xaddcom  10216  fzen  10400  fzshftral  10467  fzo0addelr  10559  flqzadd  10685  addmodidr  10762  nn0ennn  10822  ser3add  10911  bernneq2  11051  ccatrn  11325  ccatalpha  11329  shftval2  11539  shftval4  11541  crim  11571  resqrexlemover  11723  climshft2  12019  summodclem3  12094  binom1dif  12201  isumshft  12204  arisum  12212  mertenslemi1  12249  addcos  12460  demoivreALT  12488  dvdsaddr  12551  divalgb  12639  hashdvds  12946  pythagtriplem2  12992  mulgnndir  13907  cncrng  14846  ioo2bl  15545  reeff1olem  15765  ptolemy  15818  wilthlem1  15977  1sgmprm  15991  perfectlem2  15997