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

Metamath Proof Explorer

Theorem s8eqd

Description: Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses s2eqd.1 ⊢ φ → A = N
s2eqd.2 ⊢ φ → B = O
s3eqd.3 ⊢ φ → C = P
s4eqd.4 ⊢ φ → D = Q
s5eqd.5 ⊢ φ → E = R
s6eqd.6 ⊢ φ → F = S
s7eqd.6 ⊢ φ → G = T
s8eqd.6 ⊢ φ → H = U
Assertion s8eqd ⊢ φ → ⟨“ ABCDEFGH ”⟩ = ⟨“ NOPQRSTU ”⟩

Proof

Step Hyp Ref Expression
1 s2eqd.1 ⊢ φ → A = N
2 s2eqd.2 ⊢ φ → B = O
3 s3eqd.3 ⊢ φ → C = P
4 s4eqd.4 ⊢ φ → D = Q
5 s5eqd.5 ⊢ φ → E = R
6 s6eqd.6 ⊢ φ → F = S
7 s7eqd.6 ⊢ φ → G = T
8 s8eqd.6 ⊢ φ → H = U
9 1 2 3 4 5 6 7 s7eqd ⊢ φ → ⟨“ ABCDEFG ”⟩ = ⟨“ NOPQRST ”⟩
10 8 s1eqd ⊢ φ → ⟨“ H ”⟩ = ⟨“ U ”⟩
11 9 10 oveq12d ⊢ φ → ⟨“ ABCDEFG ”⟩ ++ ⟨“ H ”⟩ = ⟨“ NOPQRST ”⟩ ++ ⟨“ U ”⟩
12 df-s8 ⊢ ⟨“ ABCDEFGH ”⟩ = ⟨“ ABCDEFG ”⟩ ++ ⟨“ H ”⟩
13 df-s8 ⊢ ⟨“ NOPQRSTU ”⟩ = ⟨“ NOPQRST ”⟩ ++ ⟨“ U ”⟩
14 11 12 13 3eqtr4g ⊢ φ → ⟨“ ABCDEFGH ”⟩ = ⟨“ NOPQRSTU ”⟩