Theorem addcom 7770

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1299   ∈ wcel 1448  (class class class)co 5706  ℂcc 7498   + caddc 7503

This theorem was proved from axioms:  ax-addcom 7595

This theorem is referenced by:  addid2  7772  readdcan  7773  addcomi  7777  addcomd  7784  add12  7791  add32  7792  add42  7795  cnegexlem1  7808  cnegexlem3  7810  cnegex2  7812  subsub23  7838  pncan2  7840  addsub  7844  addsub12  7846  addsubeq4  7848  sub32  7867  pnpcan2  7873  ppncan  7875  sub4  7878  negsubdi2  7892  ltadd2  8048  ltaddnegr  8054  ltaddsub2  8066  leaddsub2  8068  leltadd  8076  ltaddpos2  8082  addge02  8102  conjmulap  8350  recreclt  8516  avgle1  8812  avgle2  8813  nn0nnaddcl  8860  xaddcom  9485  fzen  9664  fzshftral  9729  flqzadd  9912  addmodidr  9987  nn0ennn  10047  ser3add  10119  bernneq2  10254  shftval2  10439  shftval4  10441  crim  10471  resqrexlemover  10622  climshft2  10914  summodclem3  10988  binom1dif  11095  isumshft  11098  arisum  11106  mertenslemi1  11143  addcos  11251  demoivreALT  11277  dvdsaddr  11332  divalgb  11417  hashdvds  11689  ioo2bl  12462