Theorem s8eqd

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

	Ref	Expression
Hypotheses	s2eqd.1	⊢ ( 𝜑 → 𝐴 = 𝑁 )
	s2eqd.2	⊢ ( 𝜑 → 𝐵 = 𝑂 )
	s3eqd.3	⊢ ( 𝜑 → 𝐶 = 𝑃 )
	s4eqd.4	⊢ ( 𝜑 → 𝐷 = 𝑄 )
	s5eqd.5	⊢ ( 𝜑 → 𝐸 = 𝑅 )
	s6eqd.6	⊢ ( 𝜑 → 𝐹 = 𝑆 )
	s7eqd.6	⊢ ( 𝜑 → 𝐺 = 𝑇 )
	s8eqd.6	⊢ ( 𝜑 → 𝐻 = 𝑈 )
Assertion	s8eqd	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 𝑇 𝑈 ”⟩ )

Proof

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