Description: Example for df-pss . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ex-pss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ex-ss | |
|
2 | 3ex | |
|
3 | 2 | tpid3 | |
4 | 1re | |
|
5 | 1lt3 | |
|
6 | 4 5 | gtneii | |
7 | 2re | |
|
8 | 2lt3 | |
|
9 | 7 8 | gtneii | |
10 | 6 9 | nelpri | |
11 | nelne1 | |
|
12 | 3 10 11 | mp2an | |
13 | 12 | necomi | |
14 | df-pss | |
|
15 | 1 13 14 | mpbir2an | |