Theorem addcom 8156

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   + caddc 7875

This theorem was proved from axioms:  ax-addcom 7972

This theorem is referenced by:  addlid  8158  readdcan  8159  addcomi  8163  addcomd  8170  add12  8177  add32  8178  add42  8181  cnegexlem1  8194  cnegexlem3  8196  cnegex2  8198  subsub23  8224  pncan2  8226  addsub  8230  addsub12  8232  addsubeq4  8234  sub32  8253  pnpcan2  8259  ppncan  8261  sub4  8264  negsubdi2  8278  ltadd2  8438  ltaddnegr  8444  ltaddsub2  8456  leaddsub2  8458  leltadd  8466  ltaddpos2  8472  addge02  8492  conjmulap  8748  recreclt  8919  avgle1  9223  avgle2  9224  nn0nnaddcl  9271  xaddcom  9927  fzen  10109  fzshftral  10174  flqzadd  10367  addmodidr  10444  nn0ennn  10504  ser3add  10593  bernneq2  10732  shftval2  10970  shftval4  10972  crim  11002  resqrexlemover  11154  climshft2  11449  summodclem3  11523  binom1dif  11630  isumshft  11633  arisum  11641  mertenslemi1  11678  addcos  11889  demoivreALT  11917  dvdsaddr  11980  divalgb  12066  hashdvds  12359  pythagtriplem2  12404  mulgnndir  13221  cncrng  14057  ioo2bl  14711  reeff1olem  14906  ptolemy  14959  wilthlem1  15112