Theorem s5eqd

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

	Ref	Expression
Hypotheses	s2eqd.1	⊢ ( 𝜑 → 𝐴 = 𝑁 )
	s2eqd.2	⊢ ( 𝜑 → 𝐵 = 𝑂 )
	s3eqd.3	⊢ ( 𝜑 → 𝐶 = 𝑃 )
	s4eqd.4	⊢ ( 𝜑 → 𝐷 = 𝑄 )
	s5eqd.5	⊢ ( 𝜑 → 𝐸 = 𝑅 )
Assertion	s5eqd	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 𝑅 ”⟩ )

Proof

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