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

Theorem addcom 6927
Description: Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
Assertion
Ref Expression
addcom  CC  CC  +  +

Proof of Theorem addcom
StepHypRef Expression
1 ax-addcom 6763 1  CC  CC  +  +
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wceq 1242   wcel 1390  (class class class)co 5455   CCcc 6689    + caddc 6694
This theorem was proved from axioms:  ax-addcom 6763
This theorem is referenced by:  addid2  6929  readdcan  6930  addcomi  6934  addcomd  6941  add12  6946  add32  6947  add42  6950  cnegexlem1  6963  cnegexlem3  6965  cnegex2  6967  subsub23  6993  pncan2  6995  addsub  6999  addsub12  7001  addsubeq4  7003  sub32  7021  pnpcan2  7027  ppncan  7029  sub4  7032  negsubdi2  7046  ltadd2  7192  ltaddsub2  7207  leaddsub2  7209  leltadd  7217  ltaddpos2  7223  addge02  7243  conjmulap  7467  recreclt  7627  avgle1  7922  avgle2  7923  nn0nnaddcl  7969  fzen  8657  fzshftral  8720  nn0ennn  8870  bernneq2  9003  crim  9066
  Copyright terms: Public domain W3C validator