Metamath Proof Explorer

Theorem ccatw2s1ass

Description: Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 wrdv 
 |-  ( W e. Word V -> W e. Word _V )
2 s1cli 
 |-  <" X "> e. Word _V
3 2 a1i 
 |-  ( W e. Word V -> <" X "> e. Word _V )
4 s1cli 
 |-  <" Y "> e. Word _V
5 4 a1i 
 |-  ( W e. Word V -> <" Y "> e. Word _V )
6 ccatass 
 |-  ( ( W e. Word _V /\ <" X "> e. Word _V /\ <" Y "> e. Word _V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
7 1 3 5 6 syl3anc 
 |-  ( W e. Word V -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )