Metamath Proof Explorer

Theorem slotsbaseefdif

Description: The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020)

Ref Expression
Assertion slotsbaseefdif Base ndx ef ndx


Step Hyp Ref Expression
1 basendxnn Base ndx
2 1 nnrei Base ndx
3 baseltedgf Base ndx < ef ndx
4 2 3 ltneii Base ndx ef ndx