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

Metamath Proof Explorer

Theorem s7eqd

Description: Equality theorem for a length 7 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
Assertion s7eqd ⊢ φ → ⟨“ ABCDEFG ”⟩ = ⟨“ NOPQRST ”⟩

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 1 2 3 4 5 6 s6eqd ⊢ φ → ⟨“ ABCDEF ”⟩ = ⟨“ NOPQRS ”⟩
9 7 s1eqd ⊢ φ → ⟨“ G ”⟩ = ⟨“ T ”⟩
10 8 9 oveq12d ⊢ φ → ⟨“ ABCDEF ”⟩ ++ ⟨“ G ”⟩ = ⟨“ NOPQRS ”⟩ ++ ⟨“ T ”⟩
11 df-s7 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCDEF ”⟩ ++ ⟨“ G ”⟩
12 df-s7 ⊢ ⟨“ NOPQRST ”⟩ = ⟨“ NOPQRS ”⟩ ++ ⟨“ T ”⟩
13 10 11 12 3eqtr4g ⊢ φ → ⟨“ ABCDEFG ”⟩ = ⟨“ NOPQRST ”⟩