Theorem s4eqd

Description: Equality theorem for a length 4 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 )
Assertion	s4eqd	|- ( ph -> <" A B C D "> = <" N O P Q "> )

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	1 2 3	s3eqd	|- ( ph -> <" A B C "> = <" N O P "> )
6	4	s1eqd	|- ( ph -> <" D "> = <" Q "> )
7	5 6	oveq12d	|- ( ph -> ( <" A B C "> ++ <" D "> ) = ( <" N O P "> ++ <" Q "> ) )
8		df-s4	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
9		df-s4	|- <" N O P Q "> = ( <" N O P "> ++ <" Q "> )
10	7 8 9	3eqtr4g	|- ( ph -> <" A B C D "> = <" N O P Q "> )