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

Definition df-s3 12795
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 12788 . 2  class  <" A B C ">
51, 2cs2 12787 . . 3  class  <" A B ">
63cs1 12518 . . 3  class  <" C ">
7 cconcat 12517 . . 3  class concat
85, 6, 7co 6281 . 2  class  ( <" A B "> concat 
<" C "> )
94, 8wceq 1383 1  wff  <" A B C ">  =  ( <" A B "> concat  <" C "> )
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  12809  s3cld  12816  s3cli  12825  s3fv0  12834  s3fv1  12835  s3fv2  12836  s3len  12837  s4prop  12844  s3co  12850  s1s2  12852  s1s3  12853  s2s2  12858  s4s3  12860  repsw3  12870  konigsberg  24963
  Copyright terms: Public domain W3C validator