Theorem addcom 8463

Description: Addition is commutative. (Contributed by Jim Kingdon, 17-Jan-2020.)

Assertion

Ref	Expression
addcom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcom

Step	Hyp	Ref	Expression
1		ax-addcom 8279	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   + caddc 8182

This proof depends on axioms:  ax-addcom 8279

This theorem is used by:  addlid  8465  readdcan  8466  addcomi  8470  addcomd  8477  add12  8484  add32  8485  add42  8488  cnegexlem1  8501  cnegexlem3  8503  cnegex2  8505  subsub23  8531  pncan2  8533  addsub  8537  addsub12  8539  addsubeq4  8541  sub32  8560  pnpcan2  8566  ppncan  8568  sub4  8571  negsubdi2  8585  ltadd2  8747  ltaddnegr  8753  ltaddsub2  8765  leaddsub2  8767  leltadd  8775  ltaddpos2  8781  addge02  8801  conjmulap  9060  recreclt  9231  avgle1  9548  avgle2  9549  nn0nnaddcl  9596  xaddcom  10265  fzen  10449  fzshftral  10517  fzo0addelr  10609  flqzadd  10735  addmodidr  10812  nn0ennn  10872  ser3add  10961  bernneq2  11101  ccatrn  11379  ccatalpha  11383  shftval2  11593  shftval4  11595  crim  11625  resqrexlemover  11778  climshft2  12074  summodclem3  12149  binom1dif  12256  isumshft  12259  arisum  12267  mertenslemi1  12304  addcos  12515  demoivreALT  12543  dvdsaddr  12606  divalgb  12694  hashdvds  13001  pythagtriplem2  13047  mulgnndir  13956  cncrng  14908  ioo2bl  15654  reeff1olem  15874  ptolemy  15928  birthdaylem2  16094  wilthlem1  16100  1sgmprm  16114  perfectlem2  16120