![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-s3 | Structured version Visualization version Unicode version |
Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
df-s3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cC |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | cs3 12974 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | cs2 12973 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3 | cs1 12691 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
7 | cconcat 12690 |
. . 3
![]() | |
8 | 5, 6, 7 | co 6314 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wceq 1454 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |