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

Metamath Proof Explorer

Theorem s8len

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

		Ref	Expression
	Assertion	s8len	$⊢ \|⟨“ A B C D E F G H ”⟩\| = 8$

Step	Hyp	Ref	Expression
1		df-s8	$⊢ ⟨“ A B C D E F G H ”⟩ = ⟨“ A B C D E F G ”⟩ ++ ⟨“ H ”⟩$
2		s7cli	$⊢ ⟨“ A B C D E F G ”⟩ \in Word V$
3		s7len	$⊢ \|⟨“ A B C D E F G ”⟩\| = 7$
4		7p1e8	$⊢ 7 + 1 = 8$
5	1 2 3 4	cats1len	$⊢ \|⟨“ A B C D E F G H ”⟩\| = 8$