| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > df-9 | GIF version | ||
| Description: Define the number 9. (Contributed by NM, 27-May-1999.) |
| Ref | Expression |
|---|---|
| df-9 | ⊢ 9 = (8 + 1) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c9 9076 | . 2 class 9 | |
| 2 | c8 9075 | . . 3 class 8 | |
| 3 | c1 7908 | . . 3 class 1 | |
| 4 | caddc 7910 | . . 3 class + | |
| 5 | 2, 3, 4 | co 5934 | . 2 class (8 + 1) |
| 6 | 1, 5 | wceq 1372 | 1 wff 9 = (8 + 1) |
| Colors of variables: wff set class |
| This definition is referenced by: 9re 9105 9pos 9122 9m1e8 9144 8p1e9 9159 5p4e9 9167 6p3e9 9169 7p2e9 9170 9nn 9187 8lt9 9216 8p2e10 9565 9p9e18 9579 9t9e81 9614 lgsdir2lem5 15427 2lgsoddprmlem3d 15505 |
| Copyright terms: Public domain | W3C validator |