Metamath Proof Explorer


Theorem s3eqd

Description: Equality theorem for a length 3 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 )
Assertion s3eqd
|- ( ph -> <" A B C "> = <" N O P "> )

Proof

Step Hyp Ref Expression
1 s2eqd.1
 |-  ( ph -> A = N )
2 s2eqd.2
 |-  ( ph -> B = O )
3 s3eqd.3
 |-  ( ph -> C = P )
4 1 2 s2eqd
 |-  ( ph -> <" A B "> = <" N O "> )
5 3 s1eqd
 |-  ( ph -> <" C "> = <" P "> )
6 4 5 oveq12d
 |-  ( ph -> ( <" A B "> ++ <" C "> ) = ( <" N O "> ++ <" P "> ) )
7 df-s3
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
8 df-s3
 |-  <" N O P "> = ( <" N O "> ++ <" P "> )
9 6 7 8 3eqtr4g
 |-  ( ph -> <" A B C "> = <" N O P "> )