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	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		ccatws1cl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 )
2		ccatws1cl	⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 )
3	1 2	stoic3	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 )