Metamath Proof Explorer


Theorem s4fv2

Description: Extract the third symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020)

Ref Expression
Assertion s4fv2
|- ( C e. V -> ( <" A B C D "> ` 2 ) = C )

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 s3fv2
 |-  ( C e. V -> ( <" A B C "> ` 2 ) = C )
5 2nn0
 |-  2 e. NN0
6 2lt3
 |-  2 < 3
7 1 2 3 4 5 6 cats1fv
 |-  ( C e. V -> ( <" A B C D "> ` 2 ) = C )