Definition df-s3 14811

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 14804	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14803	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14558	. . 3 class ⟨“𝐶”⟩
7		cconcat 14532	. . 3 class ++
8	5, 6, 7	co 7367	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1542	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14826  s3cld  14834  s3cli  14843  s3fv0  14853  s3fv1  14854  s3fv2  14855  s3len  14856  s3tpop  14871  s4prop  14872  s3co  14883  s1s2  14885  s1s3  14886  s2s2  14891  s4s3  14893  s3s4  14895  s3eqs2s1eq  14900  repsw3  14913  s3rn  14926  2pthon3v  30011  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  nthrucw  47316