Metamath Proof Explorer


Theorem s1s4

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

Ref Expression
Assertion s1s4
|- <" A B C D E "> = ( <" A "> ++ <" B C D E "> )

Proof

Step Hyp Ref Expression
1 df-s4
 |-  <" B C D E "> = ( <" B C D "> ++ <" E "> )
2 s1cli
 |-  <" A "> e. Word _V
3 s3cli
 |-  <" B C D "> e. Word _V
4 df-s5
 |-  <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
5 s1s3
 |-  <" A B C D "> = ( <" A "> ++ <" B C D "> )
6 1 2 3 4 5 cats1cat
 |-  <" A B C D E "> = ( <" A "> ++ <" B C D E "> )