Definition df-s3 14855

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 14848	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14847	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14602	. . 3 class ⟨“𝐶”⟩
7		cconcat 14576	. . 3 class ++
8	5, 6, 7	co 7390	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1559	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14870  s3cld  14878  s3cli  14887  s3fv0  14897  s3fv1  14898  s3fv2  14899  s3len  14900  s3tpop  14915  s4prop  14916  s3co  14927  s1s2  14929  s1s3  14930  s2s2  14935  s4s3  14937  s3s4  14939  s3eqs2s1eq  14944  repsw3  14957  s3rn  14970  2pthon3v  30099  konigsberglem1  30410  konigsberglem2  30411  konigsberglem3  30412  nthrucw  47422