Theorem s8eqd

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

	Ref	Expression
Hypotheses	s2eqd.1	|- ( ph -> A = N )
	s2eqd.2	|- ( ph -> B = O )
	s3eqd.3	|- ( ph -> C = P )
	s4eqd.4	|- ( ph -> D = Q )
	s5eqd.5	|- ( ph -> E = R )
	s6eqd.6	|- ( ph -> F = S )
	s7eqd.6	|- ( ph -> G = T )
	s8eqd.6	|- ( ph -> H = U )
Assertion	s8eqd	|- ( ph -> <" A B C D E F G H "> = <" N O P Q R S T U "> )

Proof

Step	Hyp	Ref	Expression
1		s2eqd.1	|- ( ph -> A = N )
2		s2eqd.2	|- ( ph -> B = O )
3		s3eqd.3	|- ( ph -> C = P )
4		s4eqd.4	|- ( ph -> D = Q )
5		s5eqd.5	|- ( ph -> E = R )
6		s6eqd.6	|- ( ph -> F = S )
7		s7eqd.6	|- ( ph -> G = T )
8		s8eqd.6	|- ( ph -> H = U )
9	1 2 3 4 5 6 7	s7eqd	|- ( ph -> <" A B C D E F G "> = <" N O P Q R S T "> )
10	8	s1eqd	|- ( ph -> <" H "> = <" U "> )
11	9 10	oveq12d	|- ( ph -> ( <" A B C D E F G "> ++ <" H "> ) = ( <" N O P Q R S T "> ++ <" U "> ) )
12		df-s8	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
13		df-s8	|- <" N O P Q R S T U "> = ( <" N O P Q R S T "> ++ <" U "> )
14	11 12 13	3eqtr4g	|- ( ph -> <" A B C D E F G H "> = <" N O P Q R S T U "> )