This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem s4fv1

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

Ref Expression
Assertion s4fv1 ⊢ B ∈ V → ⟨“ ABCD ”⟩ ⁡ 1 = B

Proof

Step Hyp Ref Expression
1 df-s4 ⊢ ⟨“ ABCD ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩
2 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
3 s3len ⊢ ⟨“ ABC ”⟩ = 3
4 s3fv1 ⊢ B ∈ V → ⟨“ ABC ”⟩ ⁡ 1 = B
5 1nn0 ⊢ 1 ∈ ℕ 0
6 1lt3 ⊢ 1 < 3
7 1 2 3 4 5 6 cats1fv ⊢ B ∈ V → ⟨“ ABCD ”⟩ ⁡ 1 = B