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	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 ”⟩ )