Metamath Proof Explorer


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 "> )