Description: Define "all some" applied to a top-level implication, which means ps is true whenever ph is true and there is at least one x where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | df-alsi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | vx | |
|
1 | wph | |
|
2 | wps | |
|
3 | 1 2 0 | walsi | |
4 | 1 2 | wi | |
5 | 4 0 | wal | |
6 | 1 0 | wex | |
7 | 5 6 | wa | |
8 | 3 7 | wb | |