Description: A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | s2cld.1 | |- ( ph -> A e. X ) |
|
s2cld.2 | |- ( ph -> B e. X ) |
||
s3cld.3 | |- ( ph -> C e. X ) |
||
Assertion | s3cld | |- ( ph -> <" A B C "> e. Word X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s2cld.1 | |- ( ph -> A e. X ) |
|
2 | s2cld.2 | |- ( ph -> B e. X ) |
|
3 | s3cld.3 | |- ( ph -> C e. X ) |
|
4 | df-s3 | |- <" A B C "> = ( <" A B "> ++ <" C "> ) |
|
5 | 1 2 | s2cld | |- ( ph -> <" A B "> e. Word X ) |
6 | 4 5 3 | cats1cld | |- ( ph -> <" A B C "> e. Word X ) |