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 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) = ( 𝑊 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) ) |
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 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) = ( 𝑊 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) ) |