Metamath Proof Explorer

Theorem ccatw2s1cl

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

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

Step	Hyp	Ref	Expression
1		ccatws1cl	\|- ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )
2		ccatws1cl	\|- ( ( ( W ++ <" X "> ) e. Word V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V )
3	1 2	stoic3	\|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V )

Step

Hyp

Ref

Expression

 |-  ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )

 |-  ( ( ( W ++ <" X "> ) e. Word V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V )

1 2

 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V )