Metamath Proof Explorer

Theorem s3eq2

Description: Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022)

Ref Expression
Assertion s3eq2 
|- ( B = D -> <" A B C "> = <" A D C "> )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( B = D -> A = A )
2 id 
 |-  ( B = D -> B = D )
3 eqidd 
 |-  ( B = D -> C = C )
4 1 2 3 s3eqd 
 |-  ( B = D -> <" A B C "> = <" A D C "> )