![]() |
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 7744 | . 2 class 2 | |
2 | c1 6712 | . . 3 class 1 | |
3 | caddc 6714 | . . 3 class + | |
4 | 2, 2, 3 | co 5455 | . 2 class (1 + 1) |
5 | 1, 4 | wceq 1242 | 1 wff 2 = (1 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 2re 7765 0le2 7786 2pos 7787 1p1e2 7811 2p2e4 7815 2times 7816 3p2e5 7830 4p2e6 7832 5p2e7 7835 6p2e8 7839 7p2e9 7842 8p2e10 7844 2nn 7855 1lt2 7864 nneoor 8116 6p6e12 8194 7p5e12 8196 8p4e12 8200 9p2e11 8205 9p3e12 8206 eluz2b1 8315 nn01to3 8328 fztp 8710 fzprval 8714 fztpval 8715 fzo12sn 8843 sqval 8966 |
Copyright terms: Public domain | W3C validator |