Metamath Proof Explorer

Theorem s3len

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

Ref Expression
Assertion s3len 
|- ( # ` <" A B C "> ) = 3

Proof

Step Hyp Ref Expression
1 df-s3 
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
2 s2cli 
 |-  <" A B "> e. Word _V
3 s2len 
 |-  ( # ` <" A B "> ) = 2
4 2p1e3 
 |-  ( 2 + 1 ) = 3
5 1 2 3 4 cats1len 
 |-  ( # ` <" A B C "> ) = 3