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 ( 𝜑𝐴 = 𝑁 )
s2eqd.2 ( 𝜑𝐵 = 𝑂 )
s3eqd.3 ( 𝜑𝐶 = 𝑃 )
s4eqd.4 ( 𝜑𝐷 = 𝑄 )
s5eqd.5 ( 𝜑𝐸 = 𝑅 )
s6eqd.6 ( 𝜑𝐹 = 𝑆 )
Assertion s6eqd ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 ”⟩ )

Proof

Step Hyp Ref Expression
1 s2eqd.1 ( 𝜑𝐴 = 𝑁 )
2 s2eqd.2 ( 𝜑𝐵 = 𝑂 )
3 s3eqd.3 ( 𝜑𝐶 = 𝑃 )
4 s4eqd.4 ( 𝜑𝐷 = 𝑄 )
5 s5eqd.5 ( 𝜑𝐸 = 𝑅 )
6 s6eqd.6 ( 𝜑𝐹 = 𝑆 )
7 1 2 3 4 5 s5eqd ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 ”⟩ )
8 6 s1eqd ( 𝜑 → ⟨“ 𝐹 ”⟩ = ⟨“ 𝑆 ”⟩ )
9 7 8 oveq12d ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 ”⟩ ++ ⟨“ 𝐹 ”⟩ ) = ( ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 ”⟩ ++ ⟨“ 𝑆 ”⟩ ) )
10 df-s6 ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 ”⟩ ++ ⟨“ 𝐹 ”⟩ )
11 df-s6 ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 ”⟩ = ( ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 ”⟩ ++ ⟨“ 𝑆 ”⟩ )
12 9 10 11 3eqtr4g ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 ”⟩ )