Theorem ccat2s1cl

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

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

Proof

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