Theorem addcom 8309

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   + caddc 8028

This theorem was proved from axioms:  ax-addcom 8125

This theorem is referenced by:  addlid  8311  readdcan  8312  addcomi  8316  addcomd  8323  add12  8330  add32  8331  add42  8334  cnegexlem1  8347  cnegexlem3  8349  cnegex2  8351  subsub23  8377  pncan2  8379  addsub  8383  addsub12  8385  addsubeq4  8387  sub32  8406  pnpcan2  8412  ppncan  8414  sub4  8417  negsubdi2  8431  ltadd2  8592  ltaddnegr  8598  ltaddsub2  8610  leaddsub2  8612  leltadd  8620  ltaddpos2  8626  addge02  8646  conjmulap  8902  recreclt  9073  avgle1  9378  avgle2  9379  nn0nnaddcl  9426  xaddcom  10089  fzen  10271  fzshftral  10336  fzo0addelr  10427  flqzadd  10551  addmodidr  10628  nn0ennn  10688  ser3add  10777  bernneq2  10916  ccatrn  11179  ccatalpha  11183  shftval2  11380  shftval4  11382  crim  11412  resqrexlemover  11564  climshft2  11860  summodclem3  11934  binom1dif  12041  isumshft  12044  arisum  12052  mertenslemi1  12089  addcos  12300  demoivreALT  12328  dvdsaddr  12391  divalgb  12479  hashdvds  12786  pythagtriplem2  12832  mulgnndir  13731  cncrng  14576  ioo2bl  15268  reeff1olem  15488  ptolemy  15541  wilthlem1  15697  1sgmprm  15711  perfectlem2  15717