MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s3 Structured version   Unicode version

Definition df-s3 12476
Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s3  |-  <" A B C ">  =  ( <" A B "> concat  <" C "> )

Detailed syntax breakdown of Definition df-s3
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cC . . 3  class  C
41, 2, 3cs3 12469 . 2  class  <" A B C ">
51, 2cs2 12468 . . 3  class  <" A B ">
63cs1 12224 . . 3  class  <" C ">
7 cconcat 12223 . . 3  class concat
85, 6, 7co 6091 . 2  class  ( <" A B "> concat 
<" C "> )
94, 8wceq 1369 1  wff  <" A B C ">  =  ( <" A B "> concat  <" C "> )
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  12490  s3cld  12497  s3cli  12506  s3fv0  12515  s3fv1  12516  s3fv2  12517  s3len  12518  s4prop  12525  s3co  12531  s1s2  12533  s1s3  12534  s2s2  12539  s4s3  12541  repsw3  12551  konigsberg  23608
  Copyright terms: Public domain W3C validator