Metamath Proof Explorer


Theorem s6eqd

Description: Equality theorem for a length 6 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 )
s5eqd.5
|- ( ph -> E = R )
s6eqd.6
|- ( ph -> F = S )
Assertion s6eqd
|- ( ph -> <" A B C D E F "> = <" N O P Q R S "> )

Proof

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 s5eqd.5
 |-  ( ph -> E = R )
6 s6eqd.6
 |-  ( ph -> F = S )
7 1 2 3 4 5 s5eqd
 |-  ( ph -> <" A B C D E "> = <" N O P Q R "> )
8 6 s1eqd
 |-  ( ph -> <" F "> = <" S "> )
9 7 8 oveq12d
 |-  ( ph -> ( <" A B C D E "> ++ <" F "> ) = ( <" N O P Q R "> ++ <" S "> ) )
10 df-s6
 |-  <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
11 df-s6
 |-  <" N O P Q R S "> = ( <" N O P Q R "> ++ <" S "> )
12 9 10 11 3eqtr4g
 |-  ( ph -> <" A B C D E F "> = <" N O P Q R S "> )