Theorem addcom 8406

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121   + caddc 8126

This theorem was proved from axioms:  ax-addcom 8223

This theorem is referenced by:  addlid  8408  readdcan  8409  addcomi  8413  addcomd  8420  add12  8427  add32  8428  add42  8431  cnegexlem1  8444  cnegexlem3  8446  cnegex2  8448  subsub23  8474  pncan2  8476  addsub  8480  addsub12  8482  addsubeq4  8484  sub32  8503  pnpcan2  8509  ppncan  8511  sub4  8514  negsubdi2  8528  ltadd2  8689  ltaddnegr  8695  ltaddsub2  8707  leaddsub2  8709  leltadd  8717  ltaddpos2  8723  addge02  8743  conjmulap  8999  recreclt  9170  avgle1  9475  avgle2  9476  nn0nnaddcl  9523  xaddcom  10190  fzen  10373  fzshftral  10438  fzo0addelr  10530  flqzadd  10654  addmodidr  10731  nn0ennn  10791  ser3add  10880  bernneq2  11019  ccatrn  11290  ccatalpha  11294  shftval2  11504  shftval4  11506  crim  11536  resqrexlemover  11688  climshft2  11984  summodclem3  12059  binom1dif  12166  isumshft  12169  arisum  12177  mertenslemi1  12214  addcos  12425  demoivreALT  12453  dvdsaddr  12516  divalgb  12604  hashdvds  12911  pythagtriplem2  12957  mulgnndir  13857  cncrng  14704  ioo2bl  15403  reeff1olem  15623  ptolemy  15676  wilthlem1  15835  1sgmprm  15849  perfectlem2  15855