Metamath Proof Explorer


Theorem s3cld

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 )

Proof

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 )