Metamath Proof Explorer

Theorem ccatw2s1ass

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

Ref Expression
Assertion ccatw2s1ass ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩

Proof

Step Hyp Ref Expression
1 wrdv ⊢ W ∈ Word V → W ∈ Word V
2 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
3 2 a1i ⊢ W ∈ Word V → ⟨“ X ”⟩ ∈ Word V
4 s1cli ⊢ ⟨“ Y ”⟩ ∈ Word V
5 4 a1i ⊢ W ∈ Word V → ⟨“ Y ”⟩ ∈ Word V
6 ccatass ⊢ W ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V ∧ ⟨“ Y ”⟩ ∈ Word V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩
7 1 3 5 6 syl3anc ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩