Theorem addcom 8299

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   + caddc 8018

This theorem was proved from axioms:  ax-addcom 8115

This theorem is referenced by:  addlid  8301  readdcan  8302  addcomi  8306  addcomd  8313  add12  8320  add32  8321  add42  8324  cnegexlem1  8337  cnegexlem3  8339  cnegex2  8341  subsub23  8367  pncan2  8369  addsub  8373  addsub12  8375  addsubeq4  8377  sub32  8396  pnpcan2  8402  ppncan  8404  sub4  8407  negsubdi2  8421  ltadd2  8582  ltaddnegr  8588  ltaddsub2  8600  leaddsub2  8602  leltadd  8610  ltaddpos2  8616  addge02  8636  conjmulap  8892  recreclt  9063  avgle1  9368  avgle2  9369  nn0nnaddcl  9416  xaddcom  10074  fzen  10256  fzshftral  10321  fzo0addelr  10412  flqzadd  10535  addmodidr  10612  nn0ennn  10672  ser3add  10761  bernneq2  10900  ccatrn  11162  ccatalpha  11166  shftval2  11358  shftval4  11360  crim  11390  resqrexlemover  11542  climshft2  11838  summodclem3  11912  binom1dif  12019  isumshft  12022  arisum  12030  mertenslemi1  12067  addcos  12278  demoivreALT  12306  dvdsaddr  12369  divalgb  12457  hashdvds  12764  pythagtriplem2  12810  mulgnndir  13709  cncrng  14554  ioo2bl  15246  reeff1olem  15466  ptolemy  15519  wilthlem1  15675  1sgmprm  15689  perfectlem2  15695