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

Theorem 1e0p1 9455
Description: The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
Assertion
Ref Expression
1e0p1 1 = (0 + 1)

Proof of Theorem 1e0p1
StepHypRef Expression
1 0p1e1 9063 . 2 (0 + 1) = 1
21eqcomi 2193 1 1 = (0 + 1)
Colors of variables: wff set class
Syntax hints:   = wceq 1364  (class class class)co 5896  0cc0 7841  1c1 7842   + caddc 7844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171  ax-1cn 7934  ax-icn 7936  ax-addcl 7937  ax-mulcl 7939  ax-addcom 7941  ax-i2m1 7946  ax-0id 7949
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185
This theorem is referenced by:  6p5e11  9486  7p4e11  9489  8p3e11  9494  9p2e11  9500  fz1ssfz0  10147  fz0to3un2pr  10153  fzo01  10246  bcp1nk  10774  arisum2  11539  ege2le3  11711  ef4p  11734  efgt1p2  11735  efgt1p  11736  prmdiv  12267  ennnfonelem1  12458  mulgnn0p1  13073  dveflem  14644  lgsdir2lem3  14889  lgseisenlem1  14908
  Copyright terms: Public domain W3C validator