Definition df-s3 14774

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 14767	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14766	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14520	. . 3 class ⟨“𝐶”⟩
7		cconcat 14495	. . 3 class ++
8	5, 6, 7	co 7353	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1540	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14789  s3cld  14797  s3cli  14806  s3fv0  14816  s3fv1  14817  s3fv2  14818  s3len  14819  s3tpop  14834  s4prop  14835  s3co  14846  s1s2  14848  s1s3  14849  s2s2  14854  s4s3  14856  s3s4  14858  s3eqs2s1eq  14863  repsw3  14876  s3rn  14889  2pthon3v  29906  konigsberglem1  30214  konigsberglem2  30215  konigsberglem3  30216