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 \in Word V \land X \in V \land Y \in V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V$

Step	Hyp	Ref	Expression
1		ccatws1cl	$⊢ (W \in Word V \land X \in V) \to W ++ ⟨“ X ”⟩ \in Word V$
2		ccatws1cl	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land Y \in V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V$
3	1 2	stoic3	$⊢ (W \in Word V \land X \in V \land Y \in V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V$