Description: Equality theorem for a length 4 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 ) |
||
s4eqd.4 | |- ( ph -> D = Q ) |
||
Assertion | s4eqd | |- ( ph -> <" A B C D "> = <" N O P Q "> ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s2eqd.1 | |- ( ph -> A = N ) |
|
2 | s2eqd.2 | |- ( ph -> B = O ) |
|
3 | s3eqd.3 | |- ( ph -> C = P ) |
|
4 | s4eqd.4 | |- ( ph -> D = Q ) |
|
5 | 1 2 3 | s3eqd | |- ( ph -> <" A B C "> = <" N O P "> ) |
6 | 4 | s1eqd | |- ( ph -> <" D "> = <" Q "> ) |
7 | 5 6 | oveq12d | |- ( ph -> ( <" A B C "> ++ <" D "> ) = ( <" N O P "> ++ <" Q "> ) ) |
8 | df-s4 | |- <" A B C D "> = ( <" A B C "> ++ <" D "> ) |
|
9 | df-s4 | |- <" N O P Q "> = ( <" N O P "> ++ <" Q "> ) |
|
10 | 7 8 9 | 3eqtr4g | |- ( ph -> <" A B C D "> = <" N O P Q "> ) |