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

Metamath Proof Explorer

Theorem s7len

Description: The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s7len ⊢ ⟨“ ABCDEFG ”⟩ = 7

Proof

Step Hyp Ref Expression
1 df-s7 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCDEF ”⟩ ++ ⟨“ G ”⟩
2 s6cli ⊢ ⟨“ ABCDEF ”⟩ ∈ Word V
3 s6len ⊢ ⟨“ ABCDEF ”⟩ = 6
4 6p1e7 ⊢ 6 + 1 = 7
5 1 2 3 4 cats1len ⊢ ⟨“ ABCDEFG ”⟩ = 7