Metamath Proof Explorer

Theorem s4len

Description: The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s4len 
|- ( # ` <" A B C D "> ) = 4

Proof

Step Hyp Ref Expression
1 df-s4 
 |-  <" A B C D "> = ( <" A B C "> ++ <" D "> )
2 s3cli 
 |-  <" A B C "> e. Word _V
3 s3len 
 |-  ( # ` <" A B C "> ) = 3
4 3p1e4 
 |-  ( 3 + 1 ) = 4
5 1 2 3 4 cats1len 
 |-  ( # ` <" A B C D "> ) = 4