Definition df-s3 12981

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 12974	. 2 class <" A B C ">
5	1, 2	cs2 12973	. . 3 class <" A B ">
6	3	cs1 12691	. . 3 class <" C ">
7		cconcat 12690	. . 3 class ++
8	5, 6, 7	co 6314	. 2 class ( <" A B "> ++ <" C "> )
9	4, 8	wceq 1454	1 wff <" A B C "> = ( <" A B "> ++ <" C "> )

This definition is referenced by:  s3eqd  12995  s3cld  13002  s3cli  13011  s3fv0  13021  s3fv1  13022  s3fv2  13023  s3len  13024  s3tpop  13039  s4prop  13040  s3co  13051  s1s2  13053  s1s3  13054  s2s2  13059  s4s3  13061  repsw3  13074  konigsberg  25763  2pthon3v-av  39891