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

Metamath Proof Explorer

Theorem s6eqd

Description: Equality theorem for a length 6 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
Assertion s6eqd ⊢ φ → ⟨“ ABCDEF ”⟩ = ⟨“ NOPQRS ”⟩

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 1 2 3 4 5 s5eqd ⊢ φ → ⟨“ ABCDE ”⟩ = ⟨“ NOPQR ”⟩
8 6 s1eqd ⊢ φ → ⟨“ F ”⟩ = ⟨“ S ”⟩
9 7 8 oveq12d ⊢ φ → ⟨“ ABCDE ”⟩ ++ ⟨“ F ”⟩ = ⟨“ NOPQR ”⟩ ++ ⟨“ S ”⟩
10 df-s6 ⊢ ⟨“ ABCDEF ”⟩ = ⟨“ ABCDE ”⟩ ++ ⟨“ F ”⟩
11 df-s6 ⊢ ⟨“ NOPQRS ”⟩ = ⟨“ NOPQR ”⟩ ++ ⟨“ S ”⟩
12 9 10 11 3eqtr4g ⊢ φ → ⟨“ ABCDEF ”⟩ = ⟨“ NOPQRS ”⟩