Theorem ccatw2s1assOLD

Description: Obsolete version of ccatw2s1ass as of 29-Jan-2024. Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ccatw2s1assOLD	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word 𝑉 )
2		s1cl	⊢ ( 𝑋 ∈ 𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
3		s1cl	⊢ ( 𝑌 ∈ 𝑉 → ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 )
4		ccatass	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
5	1 2 3 4	syl3an	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )