This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem s8eqd

Description: Equality theorem for a length 8 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 )
s7eqd.6 
|- ( ph -> G = T )
s8eqd.6 
|- ( ph -> H = U )
Assertion s8eqd 
|- ( ph -> <" A B C D E F G H "> = <" N O P Q R S T U "> )

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 s7eqd.6 
 |-  ( ph -> G = T )
8 s8eqd.6 
 |-  ( ph -> H = U )
9 1 2 3 4 5 6 7 s7eqd 
 |-  ( ph -> <" A B C D E F G "> = <" N O P Q R S T "> )
10 8 s1eqd 
 |-  ( ph -> <" H "> = <" U "> )
11 9 10 oveq12d 
 |-  ( ph -> ( <" A B C D E F G "> ++ <" H "> ) = ( <" N O P Q R S T "> ++ <" U "> ) )
12 df-s8 
 |-  <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
13 df-s8 
 |-  <" N O P Q R S T U "> = ( <" N O P Q R S T "> ++ <" U "> )
14 11 12 13 3eqtr4g 
 |-  ( ph -> <" A B C D E F G H "> = <" N O P Q R S T U "> )