Theorem addcom 7150

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

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1243   ∈ wcel 1393  (class class class)co 5512  ℂcc 6887   + caddc 6892

This theorem was proved from axioms:  ax-addcom 6984

This theorem is referenced by:  addid2  7152  readdcan  7153  addcomi  7157  addcomd  7164  add12  7169  add32  7170  add42  7173  cnegexlem1  7186  cnegexlem3  7188  cnegex2  7190  subsub23  7216  pncan2  7218  addsub  7222  addsub12  7224  addsubeq4  7226  sub32  7245  pnpcan2  7251  ppncan  7253  sub4  7256  negsubdi2  7270  ltadd2  7416  ltaddsub2  7432  leaddsub2  7434  leltadd  7442  ltaddpos2  7448  addge02  7468  conjmulap  7705  recreclt  7866  avgle1  8165  avgle2  8166  nn0nnaddcl  8213  fzen  8907  fzshftral  8970  flqzadd  9140  nn0ennn  9209  iseradd  9243  bernneq2  9370  shftval2  9427  shftval4  9429  crim  9458  resqrexlemover  9608  climshft2  9827