Metamath Proof Explorer

Theorem ccatw2s1ccatws2OLD

Description: Obsolete version of ccatw2s1ccatws2 as of 29-Jan-2024. The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton word consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ccatw2s1ccatws2OLD 
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ <" X Y "> ) )

Proof

Step Hyp Ref Expression
1 ccatw2s1assOLD 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
2 df-s2 
 |-  <" X Y "> = ( <" X "> ++ <" Y "> )
3 2 a1i 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> <" X Y "> = ( <" X "> ++ <" Y "> ) )
4 3 eqcomd 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( <" X "> ++ <" Y "> ) = <" X Y "> )
5 4 oveq2d 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( W ++ ( <" X "> ++ <" Y "> ) ) = ( W ++ <" X Y "> ) )
6 1 5 eqtrd 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ <" X Y "> ) )