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

Metamath Proof Explorer

Theorem s8cld

Description: A length 8 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses s2cld.1 ⊢ φ → A ∈ X
s2cld.2 ⊢ φ → B ∈ X
s3cld.3 ⊢ φ → C ∈ X
s4cld.4 ⊢ φ → D ∈ X
s5cld.5 ⊢ φ → E ∈ X
s6cld.6 ⊢ φ → F ∈ X
s7cld.7 ⊢ φ → G ∈ X
s8cld.8 ⊢ φ → H ∈ X
Assertion s8cld ⊢ φ → ⟨“ ABCDEFGH ”⟩ ∈ Word X

Proof

Step Hyp Ref Expression
1 s2cld.1 ⊢ φ → A ∈ X
2 s2cld.2 ⊢ φ → B ∈ X
3 s3cld.3 ⊢ φ → C ∈ X
4 s4cld.4 ⊢ φ → D ∈ X
5 s5cld.5 ⊢ φ → E ∈ X
6 s6cld.6 ⊢ φ → F ∈ X
7 s7cld.7 ⊢ φ → G ∈ X
8 s8cld.8 ⊢ φ → H ∈ X
9 df-s8 ⊢ ⟨“ ABCDEFGH ”⟩ = ⟨“ ABCDEFG ”⟩ ++ ⟨“ H ”⟩
10 1 2 3 4 5 6 7 s7cld ⊢ φ → ⟨“ ABCDEFG ”⟩ ∈ Word X
11 9 10 8 cats1cld ⊢ φ → ⟨“ ABCDEFGH ”⟩ ∈ Word X