Definition df-s3

Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	df-s3	⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3	0 1 2	cs3	⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩
4	0 1	cs2	⊢ ⟨“ 𝐴 𝐵 ”⟩
5		cconcat	⊢ ++
6	2	cs1	⊢ ⟨“ 𝐶 ”⟩
7	4 6 5	co	⊢ ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ )
8	3 7	wceq	⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ )