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 ∈ Word V ∧ X ∈ V ∧ Y ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V

Proof

Step Hyp Ref Expression
1 ccatws1cl ⊢ W ∈ Word V ∧ X ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V
2 ccatws1cl ⊢ W ++ ⟨“ X ”⟩ ∈ Word V ∧ Y ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V
3 1 2 stoic3 ⊢ W ∈ Word V ∧ X ∈ V ∧ Y ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V