Description: The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | basendxnedgfndx | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | basendxnn | |
|
2 | 1 | nnrei | |
3 | basendxltedgfndx | |
|
4 | 2 3 | ltneii | |