Description: The positive fraction 'one'. (Contributed by NM, 29-Oct-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 1nq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1nq | |
|
2 | 1pi | |
|
3 | pinq | |
|
4 | 2 3 | ax-mp | |
5 | 1 4 | eqeltri | |