Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | s1eqd.1 | |- ( ph -> A = B ) |
|
Assertion | s1eqd | |- ( ph -> <" A "> = <" B "> ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s1eqd.1 | |- ( ph -> A = B ) |
|
2 | s1eq | |- ( A = B -> <" A "> = <" B "> ) |
|
3 | 1 2 | syl | |- ( ph -> <" A "> = <" B "> ) |