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

Theorem 1e0p1 9174
 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 8791 . 2 (0 + 1) = 1
21eqcomi 2119 1 1 = (0 + 1)
 Colors of variables: wff set class Syntax hints:   = wceq 1314  (class class class)co 5740  0cc0 7584  1c1 7585   + caddc 7587 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097  ax-1cn 7677  ax-icn 7679  ax-addcl 7680  ax-mulcl 7682  ax-addcom 7684  ax-i2m1 7689  ax-0id 7692 This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111 This theorem is referenced by:  6p5e11  9205  7p4e11  9208  8p3e11  9213  9p2e11  9219  fz1ssfz0  9837  fzo01  9933  bcp1nk  10448  arisum2  11208  ege2le3  11276  ef4p  11299  efgt1p2  11300  efgt1p  11301  ennnfonelem1  11815  dveflem  12738
 Copyright terms: Public domain W3C validator