Definition df-s3 14815

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 14808	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14807	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14560	. . 3 class ⟨“𝐶”⟩
7		cconcat 14535	. . 3 class ++
8	5, 6, 7	co 7387	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1540	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14830  s3cld  14838  s3cli  14847  s3fv0  14857  s3fv1  14858  s3fv2  14859  s3len  14860  s3tpop  14875  s4prop  14876  s3co  14887  s1s2  14889  s1s3  14890  s2s2  14895  s4s3  14897  s3s4  14899  s3eqs2s1eq  14904  repsw3  14917  s3rn  14930  2pthon3v  29873  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183