Definition df-s3 13594

Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-s3	|- <" A B C "> = ( <" A B "> ++ <" C "> )

Detailed syntax breakdown of Definition df-s3

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cC	. . 3 class C
4	1, 2, 3	cs3 13587	. 2 class <" A B C ">
5	1, 2	cs2 13586	. . 3 class <" A B ">
6	3	cs1 13294	. . 3 class <" C ">
7		cconcat 13293	. . 3 class ++
8	5, 6, 7	co 6650	. 2 class ( <" A B "> ++ <" C "> )
9	4, 8	wceq 1483	1 wff <" A B C "> = ( <" A B "> ++ <" C "> )

This definition is referenced by:  s3eqd  13609  s3cld  13617  s3cli  13626  s3fv0  13636  s3fv1  13637  s3fv2  13638  s3len  13639  s3tpop  13654  s4prop  13655  s3co  13666  s1s2  13668  s1s3  13669  s2s2  13674  s4s3  13676  s3s4  13678  s3eqs2s1eq  13683  repsw3  13694  2pthon3v  26839  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116