Theorem addcom 8291

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   + caddc 8010

This theorem was proved from axioms:  ax-addcom 8107

This theorem is referenced by:  addlid  8293  readdcan  8294  addcomi  8298  addcomd  8305  add12  8312  add32  8313  add42  8316  cnegexlem1  8329  cnegexlem3  8331  cnegex2  8333  subsub23  8359  pncan2  8361  addsub  8365  addsub12  8367  addsubeq4  8369  sub32  8388  pnpcan2  8394  ppncan  8396  sub4  8399  negsubdi2  8413  ltadd2  8574  ltaddnegr  8580  ltaddsub2  8592  leaddsub2  8594  leltadd  8602  ltaddpos2  8608  addge02  8628  conjmulap  8884  recreclt  9055  avgle1  9360  avgle2  9361  nn0nnaddcl  9408  xaddcom  10065  fzen  10247  fzshftral  10312  fzo0addelr  10403  flqzadd  10526  addmodidr  10603  nn0ennn  10663  ser3add  10752  bernneq2  10891  ccatrn  11152  shftval2  11345  shftval4  11347  crim  11377  resqrexlemover  11529  climshft2  11825  summodclem3  11899  binom1dif  12006  isumshft  12009  arisum  12017  mertenslemi1  12054  addcos  12265  demoivreALT  12293  dvdsaddr  12356  divalgb  12444  hashdvds  12751  pythagtriplem2  12797  mulgnndir  13696  cncrng  14541  ioo2bl  15233  reeff1olem  15453  ptolemy  15506  wilthlem1  15662  1sgmprm  15676  perfectlem2  15682