Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-2 | GIF version |
Description: Define the number 2. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-2 | ⊢ 2 = (1 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2 7964 | . 2 class 2 | |
2 | c1 6890 | . . 3 class 1 | |
3 | caddc 6892 | . . 3 class + | |
4 | 2, 2, 3 | co 5512 | . 2 class (1 + 1) |
5 | 1, 4 | wceq 1243 | 1 wff 2 = (1 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 2re 7985 0le2 8006 2pos 8007 1p1e2 8033 2p2e4 8037 2times 8038 3p2e5 8052 4p2e6 8054 5p2e7 8057 6p2e8 8061 7p2e9 8064 8p2e10 8066 2nn 8077 1lt2 8086 nneoor 8340 6p6e12 8418 7p5e12 8420 8p4e12 8424 9p2e11 8429 9p3e12 8430 eluz2b1 8539 nn01to3 8552 fztp 8940 fzprval 8944 fztpval 8945 fzo12sn 9073 rebtwn2zlemstep 9107 rebtwn2z 9109 sqval 9312 ex-fl 9895 |
Copyright terms: Public domain | W3C validator |