Description: The image by S of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ballotth.m | |
|
ballotth.n | |
||
ballotth.o | |
||
ballotth.p | |
||
ballotth.f | |
||
ballotth.e | |
||
ballotth.mgtn | |
||
ballotth.i | |
||
ballotth.s | |
||
Assertion | ballotlemsi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ballotth.m | |
|
2 | ballotth.n | |
|
3 | ballotth.o | |
|
4 | ballotth.p | |
|
5 | ballotth.f | |
|
6 | ballotth.e | |
|
7 | ballotth.mgtn | |
|
8 | ballotth.i | |
|
9 | ballotth.s | |
|
10 | 1 2 3 4 5 6 7 8 | ballotlemiex | |
11 | 10 | simpld | |
12 | 1 2 3 4 5 6 7 8 9 | ballotlemsv | |
13 | 11 12 | mpdan | |
14 | elfzelz | |
|
15 | 14 | zred | |
16 | 11 15 | syl | |
17 | 16 | leidd | |
18 | 17 | iftrued | |
19 | 16 | recnd | |
20 | 1cnd | |
|
21 | 19 20 | pncan2d | |
22 | 13 18 21 | 3eqtrd | |