ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addcom GIF version

Theorem addcom 7210
Description: Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
Assertion
Ref Expression
addcom ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcom
StepHypRef Expression
1 ax-addcom 7041 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101   = wceq 1259  wcel 1409  (class class class)co 5539  cc 6944   + caddc 6949
This theorem was proved from axioms:  ax-addcom 7041
This theorem is referenced by:  addid2  7212  readdcan  7213  addcomi  7217  addcomd  7224  add12  7231  add32  7232  add42  7235  cnegexlem1  7248  cnegexlem3  7250  cnegex2  7252  subsub23  7278  pncan2  7280  addsub  7284  addsub12  7286  addsubeq4  7288  sub32  7307  pnpcan2  7313  ppncan  7315  sub4  7318  negsubdi2  7332  ltadd2  7487  ltaddnegr  7493  ltaddsub2  7505  leaddsub2  7507  leltadd  7515  ltaddpos2  7521  addge02  7541  conjmulap  7779  recreclt  7940  avgle1  8221  avgle2  8222  nn0nnaddcl  8269  fzen  9008  fzshftral  9071  flqzadd  9247  addmodidr  9322  nn0ennn  9372  iseradd  9406  bernneq2  9537  shftval2  9654  shftval4  9656  crim  9685  resqrexlemover  9836  climshft2  10057  dvdsaddr  10150
  Copyright terms: Public domain W3C validator