Definition df-s3 14758

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 14751	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14750	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14505	. . 3 class ⟨“𝐶”⟩
7		cconcat 14479	. . 3 class ++
8	5, 6, 7	co 7352	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1541	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14773  s3cld  14781  s3cli  14790  s3fv0  14800  s3fv1  14801  s3fv2  14802  s3len  14803  s3tpop  14818  s4prop  14819  s3co  14830  s1s2  14832  s1s3  14833  s2s2  14838  s4s3  14840  s3s4  14842  s3eqs2s1eq  14847  repsw3  14860  s3rn  14873  2pthon3v  29923  konigsberglem1  30234  konigsberglem2  30235  konigsberglem3  30236  nthrucw  47009