Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 29-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme21.l | |
|
cdleme21.j | |
||
cdleme21.m | |
||
cdleme21.a | |
||
cdleme21.h | |
||
cdleme21.u | |
||
Assertion | cdleme21at | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme21.l | |
|
2 | cdleme21.j | |
|
3 | cdleme21.m | |
|
4 | cdleme21.a | |
|
5 | cdleme21.h | |
|
6 | cdleme21.u | |
|
7 | 1 2 3 4 5 6 | cdleme21c | |
8 | 7 | 3adant2r | |
9 | simp2r | |
|
10 | oveq2 | |
|
11 | 10 | breq2d | |
12 | 9 11 | syl5ibcom | |
13 | 12 | necon3bd | |
14 | 8 13 | mpd | |