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

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

Proof of Theorem addcom
StepHypRef Expression
1 ax-addcom 7348 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1285  wcel 1434  (class class class)co 5591  cc 7251   + caddc 7256
This theorem was proved from axioms:  ax-addcom 7348
This theorem is referenced by:  addid2  7524  readdcan  7525  addcomi  7529  addcomd  7536  add12  7543  add32  7544  add42  7547  cnegexlem1  7560  cnegexlem3  7562  cnegex2  7564  subsub23  7590  pncan2  7592  addsub  7596  addsub12  7598  addsubeq4  7600  sub32  7619  pnpcan2  7625  ppncan  7627  sub4  7630  negsubdi2  7644  ltadd2  7800  ltaddnegr  7806  ltaddsub2  7818  leaddsub2  7820  leltadd  7828  ltaddpos2  7834  addge02  7854  conjmulap  8094  recreclt  8255  avgle1  8548  avgle2  8549  nn0nnaddcl  8596  fzen  9352  fzshftral  9415  flqzadd  9594  addmodidr  9669  nn0ennn  9729  iseradd  9778  bernneq2  9910  shftval2  10088  shftval4  10090  crim  10119  resqrexlemover  10270  climshft2  10519  dvdsaddr  10620  divalgb  10705  hashdvds  10977
  Copyright terms: Public domain W3C validator