| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 2nn | Structured version Visualization version GIF version | ||
| Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
| Ref | Expression |
|---|---|
| 2nn | ⊢ 2 ∈ ℕ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-2 12329 | . 2 ⊢ 2 = (1 + 1) | |
| 2 | 1nn 12277 | . . 3 ⊢ 1 ∈ ℕ | |
| 3 | peano2nn 12278 | . . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ) | |
| 4 | 2, 3 | ax-mp 5 | . 2 ⊢ (1 + 1) ∈ ℕ |
| 5 | 1, 4 | eqeltri 2837 | 1 ⊢ 2 ∈ ℕ |
| Copyright terms: Public domain | W3C validator |