Theorem addcom 8316

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035

This theorem was proved from axioms:  ax-addcom 8132

This theorem is referenced by:  addlid  8318  readdcan  8319  addcomi  8323  addcomd  8330  add12  8337  add32  8338  add42  8341  cnegexlem1  8354  cnegexlem3  8356  cnegex2  8358  subsub23  8384  pncan2  8386  addsub  8390  addsub12  8392  addsubeq4  8394  sub32  8413  pnpcan2  8419  ppncan  8421  sub4  8424  negsubdi2  8438  ltadd2  8599  ltaddnegr  8605  ltaddsub2  8617  leaddsub2  8619  leltadd  8627  ltaddpos2  8633  addge02  8653  conjmulap  8909  recreclt  9080  avgle1  9385  avgle2  9386  nn0nnaddcl  9433  xaddcom  10096  fzen  10278  fzshftral  10343  fzo0addelr  10435  flqzadd  10559  addmodidr  10636  nn0ennn  10696  ser3add  10785  bernneq2  10924  ccatrn  11187  ccatalpha  11191  shftval2  11388  shftval4  11390  crim  11420  resqrexlemover  11572  climshft2  11868  summodclem3  11943  binom1dif  12050  isumshft  12053  arisum  12061  mertenslemi1  12098  addcos  12309  demoivreALT  12337  dvdsaddr  12400  divalgb  12488  hashdvds  12795  pythagtriplem2  12841  mulgnndir  13740  cncrng  14586  ioo2bl  15278  reeff1olem  15498  ptolemy  15551  wilthlem1  15707  1sgmprm  15721  perfectlem2  15727