Theorem s7eqd

Description: Equality theorem for a length 7 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	⊢ ( 𝜑 → 𝐺 = 𝑇 )
Assertion	s7eqd	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 𝑇 ”⟩ )

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	1 2 3 4 5 6	s6eqd	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 ”⟩ )
9	7	s1eqd	⊢ ( 𝜑 → ⟨“ 𝐺 ”⟩ = ⟨“ 𝑇 ”⟩ )
10	8 9	oveq12d	⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ++ ⟨“ 𝐺 ”⟩ ) = ( ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 ”⟩ ++ ⟨“ 𝑇 ”⟩ ) )
11		df-s7	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ++ ⟨“ 𝐺 ”⟩ )
12		df-s7	⊢ ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 𝑇 ”⟩ = ( ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 ”⟩ ++ ⟨“ 𝑇 ”⟩ )
13	10 11 12	3eqtr4g	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 𝑆 𝑇 ”⟩ )