Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-s4 | Structured version Visualization version Unicode version |
Description: Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
df-s4 | ++ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cC | . . 3 | |
4 | cD | . . 3 | |
5 | 1, 2, 3, 4 | cs4 13588 | . 2 |
6 | 1, 2, 3 | cs3 13587 | . . 3 |
7 | 4 | cs1 13294 | . . 3 |
8 | cconcat 13293 | . . 3 ++ | |
9 | 6, 7, 8 | co 6650 | . 2 ++ |
10 | 5, 9 | wceq 1483 | 1 ++ |
Colors of variables: wff setvar class |
This definition is referenced by: s4eqd 13610 s4cld 13618 s4cli 13627 s4fv0 13640 s4fv1 13641 s4fv2 13642 s4fv3 13643 s4len 13644 s4prop 13655 s1s3 13669 s1s4 13670 s2s2 13674 s4s4 13677 tgcgr4 25426 konigsberglem1 27114 konigsberglem2 27115 konigsberglem3 27116 |
Copyright terms: Public domain | W3C validator |