Definition df-s3 14772

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 14765	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14764	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14519	. . 3 class ⟨“𝐶”⟩
7		cconcat 14493	. . 3 class ++
8	5, 6, 7	co 7358	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1541	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14787  s3cld  14795  s3cli  14804  s3fv0  14814  s3fv1  14815  s3fv2  14816  s3len  14817  s3tpop  14832  s4prop  14833  s3co  14844  s1s2  14846  s1s3  14847  s2s2  14852  s4s3  14854  s3s4  14856  s3eqs2s1eq  14861  repsw3  14874  s3rn  14887  2pthon3v  30016  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  nthrucw  47126