Theorem s2eqd

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

	Ref	Expression
Hypotheses	s2eqd.1	|- ( ph -> A = N )
	s2eqd.2	|- ( ph -> B = O )
Assertion	s2eqd	|- ( ph -> <" A B "> = <" N O "> )

Proof

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