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

Metamath Proof Explorer

Theorem s4s3

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

Ref Expression
Assertion s4s3 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩

Proof

Step Hyp Ref Expression
1 df-s3 ⊢ ⟨“ EFG ”⟩ = ⟨“ EF ”⟩ ++ ⟨“ G ”⟩
2 s4cli ⊢ ⟨“ ABCD ”⟩ ∈ Word V
3 s2cli ⊢ ⟨“ EF ”⟩ ∈ Word V
4 df-s7 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCDEF ”⟩ ++ ⟨“ G ”⟩
5 s4s2 ⊢ ⟨“ ABCDEF ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EF ”⟩
6 1 2 3 4 5 cats1cat ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩