Metamath Proof Explorer

Theorem lennncl

Description: The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Assertion lennncl W Word S W W


Step Hyp Ref Expression
1 wrdfin W Word S W Fin
2 hashnncl W Fin W W
3 1 2 syl W Word S W W
4 3 biimpar W Word S W W