Theorem addcom 8251

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965   + caddc 7970

This theorem was proved from axioms:  ax-addcom 8067

This theorem is referenced by:  addlid  8253  readdcan  8254  addcomi  8258  addcomd  8265  add12  8272  add32  8273  add42  8276  cnegexlem1  8289  cnegexlem3  8291  cnegex2  8293  subsub23  8319  pncan2  8321  addsub  8325  addsub12  8327  addsubeq4  8329  sub32  8348  pnpcan2  8354  ppncan  8356  sub4  8359  negsubdi2  8373  ltadd2  8534  ltaddnegr  8540  ltaddsub2  8552  leaddsub2  8554  leltadd  8562  ltaddpos2  8568  addge02  8588  conjmulap  8844  recreclt  9015  avgle1  9320  avgle2  9321  nn0nnaddcl  9368  xaddcom  10025  fzen  10207  fzshftral  10272  fzo0addelr  10362  flqzadd  10485  addmodidr  10562  nn0ennn  10622  ser3add  10711  bernneq2  10850  ccatrn  11110  shftval2  11303  shftval4  11305  crim  11335  resqrexlemover  11487  climshft2  11783  summodclem3  11857  binom1dif  11964  isumshft  11967  arisum  11975  mertenslemi1  12012  addcos  12223  demoivreALT  12251  dvdsaddr  12314  divalgb  12402  hashdvds  12709  pythagtriplem2  12755  mulgnndir  13654  cncrng  14498  ioo2bl  15190  reeff1olem  15410  ptolemy  15463  wilthlem1  15619  1sgmprm  15633  perfectlem2  15639