Description: Natural deduction form of specialized suprlub . (Contributed by Stanislas Polu, 9-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | suprlubrd.1 | |
|
suprlubrd.2 | |
||
suprlubrd.3 | |
||
suprlubrd.4 | |
||
suprlubrd.5 | |
||
Assertion | suprlubrd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suprlubrd.1 | |
|
2 | suprlubrd.2 | |
|
3 | suprlubrd.3 | |
|
4 | suprlubrd.4 | |
|
5 | suprlubrd.5 | |
|
6 | suprlub | |
|
7 | 1 2 3 4 6 | syl31anc | |
8 | 7 | bicomd | |
9 | 8 | biimpd | |
10 | 9 | imp | |
11 | 5 10 | mpdan | |