![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1e0p1 | GIF version |
Description: The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Ref | Expression |
---|---|
1e0p1 | ⊢ 1 = (0 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0p1e1 9063 | . 2 ⊢ (0 + 1) = 1 | |
2 | 1 | eqcomi 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 |