Metamath Proof Explorer
Description: Index value of the "line" slot. Use ndxarg . (Contributed by Thierry
Arnoux, 27-Mar-2019) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
lngndx |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
df-lng |
|
2 |
|
1nn0 |
|
3 |
|
7nn |
|
4 |
2 3
|
decnncl |
|
5 |
1 4
|
ndxarg |
|