Theorem ccatw2s1assOLD

Description: Obsolete version of ccatw2s1ass as of 29-Jan-2024. Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		id	|- ( W e. Word V -> W e. Word V )
2		s1cl	|- ( X e. V -> <" X "> e. Word V )
3		s1cl	|- ( Y e. V -> <" Y "> e. Word V )
4		ccatass	|- ( ( W e. Word V /\ <" X "> e. Word V /\ <" Y "> e. Word V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
5	1 2 3 4	syl3an	|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )