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

Proof

Step	Hyp	Ref	Expression
1		wrdv	⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V )
2		s1cli	⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
3	2	a1i	⊢ ( 𝑊 ∈ Word 𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word V )
4		s1cli	⊢ ⟨“ 𝑌 ”⟩ ∈ Word V
5	4	a1i	⊢ ( 𝑊 ∈ Word 𝑉 → ⟨“ 𝑌 ”⟩ ∈ Word V )
6		ccatass	⊢ ( ( 𝑊 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
7	1 3 5 6	syl3anc	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )