Description: TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? TODO: The .\/ hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemg5.l | |
|
cdlemg5.j | |
||
cdlemg5.a | |
||
cdlemg5.h | |
||
Assertion | cdlemg5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemg5.l | |
|
2 | cdlemg5.j | |
|
3 | cdlemg5.a | |
|
4 | cdlemg5.h | |
|
5 | 1 3 4 | lhpexle | |
6 | 5 | adantr | |
7 | simpll | |
|
8 | simpr | |
|
9 | simplr | |
|
10 | 1 2 3 4 | cdlemf1 | |
11 | 7 8 9 10 | syl3anc | |
12 | 3simpa | |
|
13 | 12 | reximi | |
14 | 11 13 | syl | |
15 | 6 14 | rexlimddv | |