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

Definition df-s3 12814
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
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cC . . 3
41, 2, 3cs3 12807 . 2
51, 2cs2 12806 . . 3
63cs1 12537 . . 3
7 cconcat 12536 . . 3
85, 6, 7co 6296 . 2
94, 8wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  12828  s3cld  12835  s3cli  12844  s3fv0  12853  s3fv1  12854  s3fv2  12855  s3len  12856  s4prop  12863  s3co  12869  s1s2  12871  s1s3  12872  s2s2  12877  s4s3  12879  repsw3  12889  konigsberg  24987
  Copyright terms: Public domain W3C validator