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