Definition df-s3 14784

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

Assertion

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

Detailed syntax breakdown of Definition df-s3

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cC	. . 3 class 𝐶
4	1, 2, 3	cs3 14777	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14776	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14531	. . 3 class ⟨“𝐶”⟩
7		cconcat 14505	. . 3 class ++
8	5, 6, 7	co 7368	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1542	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14799  s3cld  14807  s3cli  14816  s3fv0  14826  s3fv1  14827  s3fv2  14828  s3len  14829  s3tpop  14844  s4prop  14845  s3co  14856  s1s2  14858  s1s3  14859  s2s2  14864  s4s3  14866  s3s4  14868  s3eqs2s1eq  14873  repsw3  14886  s3rn  14899  2pthon3v  30028  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  nthrucw  47241