Description: There exists an atom under a co-atom. (Contributed by NM, 26-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lhp2a.l | |
|
lhp2a.a | |
||
lhp2a.h | |
||
Assertion | lhpexle | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhp2a.l | |
|
2 | lhp2a.a | |
|
3 | lhp2a.h | |
|
4 | simpl | |
|
5 | eqid | |
|
6 | 5 3 | lhpbase | |
7 | 6 | adantl | |
8 | eqid | |
|
9 | 8 3 | lhpn0 | |
10 | 5 1 8 2 | atle | |
11 | 4 7 9 10 | syl3anc | |