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

Metamath Proof Explorer

Theorem s4s2

Description: Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s4s2 ⊢ ⟨“ ABCDEF ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EF ”⟩

Proof

Step Hyp Ref Expression
1 df-s2 ⊢ ⟨“ EF ”⟩ = ⟨“ E ”⟩ ++ ⟨“ F ”⟩
2 s4cli ⊢ ⟨“ ABCD ”⟩ ∈ Word V
3 s1cli ⊢ ⟨“ E ”⟩ ∈ Word V
4 df-s6 ⊢ ⟨“ ABCDEF ”⟩ = ⟨“ ABCDE ”⟩ ++ ⟨“ F ”⟩
5 df-s5 ⊢ ⟨“ ABCDE ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ E ”⟩
6 1 2 3 4 5 cats1cat ⊢ ⟨“ ABCDEF ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EF ”⟩