Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Nov-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme0.l | |
|
cdleme0.j | |
||
cdleme0.m | |
||
cdleme0.a | |
||
cdleme0.h | |
||
cdleme0.u | |
||
Assertion | cdleme02N | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme0.l | |
|
2 | cdleme0.j | |
|
3 | cdleme0.m | |
|
4 | cdleme0.a | |
|
5 | cdleme0.h | |
|
6 | cdleme0.u | |
|
7 | 1 2 3 4 5 6 | cdleme01N | |
8 | simp1l | |
|
9 | hlcvl | |
|
10 | 8 9 | syl | |
11 | simp2ll | |
|
12 | simp2rl | |
|
13 | simp1 | |
|
14 | simp2l | |
|
15 | simp3 | |
|
16 | 1 2 3 4 5 6 | lhpat2 | |
17 | 13 14 12 15 16 | syl112anc | |
18 | 4 1 2 | cvlsupr2 | |
19 | 10 11 12 17 15 18 | syl131anc | |
20 | 19 | anbi1d | |
21 | 7 20 | mpbird | |