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 CV⟨“ABCD”⟩2=C

Proof

Step Hyp Ref Expression
1 df-s4 ⟨“ABCD”⟩=⟨“ABC”⟩++⟨“D”⟩
2 s3cli ⟨“ABC”⟩WordV
3 s3len ⟨“ABC”⟩=3
4 s3fv2 CV⟨“ABC”⟩2=C
5 2nn0 20
6 2lt3 2<3
7 1 2 3 4 5 6 cats1fv CV⟨“ABCD”⟩2=C