Definition df-s3 14802

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 14795	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14794	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14549	. . 3 class ⟨“𝐶”⟩
7		cconcat 14523	. . 3 class ++
8	5, 6, 7	co 7360	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1542	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14817  s3cld  14825  s3cli  14834  s3fv0  14844  s3fv1  14845  s3fv2  14846  s3len  14847  s3tpop  14862  s4prop  14863  s3co  14874  s1s2  14876  s1s3  14877  s2s2  14882  s4s3  14884  s3s4  14886  s3eqs2s1eq  14891  repsw3  14904  s3rn  14917  2pthon3v  30026  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  nthrucw  47332