Theorem s3eqd

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

Proof

Step	Hyp	Ref	Expression
1		s2eqd.1	|- ( ph -> A = N )
2		s2eqd.2	|- ( ph -> B = O )
3		s3eqd.3	|- ( ph -> C = P )
4	1 2	s2eqd	|- ( ph -> <" A B "> = <" N O "> )
5	3	s1eqd	|- ( ph -> <" C "> = <" P "> )
6	4 5	oveq12d	|- ( ph -> ( <" A B "> ++ <" C "> ) = ( <" N O "> ++ <" P "> ) )
7		df-s3	|- <" A B C "> = ( <" A B "> ++ <" C "> )
8		df-s3	|- <" N O P "> = ( <" N O "> ++ <" P "> )
9	6 7 8	3eqtr4g	|- ( ph -> <" A B C "> = <" N O P "> )