Metamath Proof Explorer

Theorem s8cli

Description: A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s8cli 
|- <" A B C D E F G H "> e. Word _V

Proof

Step Hyp Ref Expression
1 df-s8 
 |-  <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
2 s7cli 
 |-  <" A B C D E F G "> e. Word _V
3 1 2 cats1cli 
 |-  <" A B C D E F G H "> e. Word _V