Definition df-s3 14809

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 14802	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14801	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14556	. . 3 class ⟨“𝐶”⟩
7		cconcat 14530	. . 3 class ++
8	5, 6, 7	co 7363	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1547	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14824  s3cld  14832  s3cli  14841  s3fv0  14851  s3fv1  14852  s3fv2  14853  s3len  14854  s3tpop  14869  s4prop  14870  s3co  14881  s1s2  14883  s1s3  14884  s2s2  14889  s4s3  14891  s3s4  14893  s3eqs2s1eq  14898  repsw3  14911  s3rn  14924  2pthon3v  30036  konigsberglem1  30347  konigsberglem2  30348  konigsberglem3  30349  nthrucw  47338