Metamath Proof Explorer

Theorem s1s2

Description: Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s1s2 
|- <" A B C "> = ( <" A "> ++ <" B C "> )

Proof

Step Hyp Ref Expression
1 df-s2 
 |-  <" B C "> = ( <" B "> ++ <" C "> )
2 s1cli 
 |-  <" A "> e. Word _V
3 s1cli 
 |-  <" B "> e. Word _V
4 df-s3 
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
5 df-s2 
 |-  <" A B "> = ( <" A "> ++ <" B "> )
6 1 2 3 4 5 cats1cat 
 |-  <" A B C "> = ( <" A "> ++ <" B C "> )