Description: Part of proof of Lemma K of Crawley p. 118. TODO: Eliminate and put into cdlemksel . (Contributed by NM, 25-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemk.b | |
|
cdlemk.l | |
||
cdlemk.j | |
||
cdlemk.a | |
||
cdlemk.h | |
||
cdlemk.t | |
||
cdlemk.r | |
||
cdlemk.m | |
||
cdlemk.i | |
||
Assertion | cdlemki | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemk.b | |
|
2 | cdlemk.l | |
|
3 | cdlemk.j | |
|
4 | cdlemk.a | |
|
5 | cdlemk.h | |
|
6 | cdlemk.t | |
|
7 | cdlemk.r | |
|
8 | cdlemk.m | |
|
9 | cdlemk.i | |
|
10 | simp11 | |
|
11 | simp22 | |
|
12 | simp1 | |
|
13 | simp21 | |
|
14 | 2 4 5 6 | ltrnel | |
15 | 10 13 11 14 | syl3anc | |
16 | simp11l | |
|
17 | simp22l | |
|
18 | 14 | simpld | |
19 | 10 13 11 18 | syl3anc | |
20 | 2 3 4 | hlatlej2 | |
21 | 16 17 19 20 | syl3anc | |
22 | simp23 | |
|
23 | 22 | oveq2d | |
24 | 2 3 4 5 6 7 | trljat1 | |
25 | 10 13 11 24 | syl3anc | |
26 | 23 25 | eqtr2d | |
27 | 21 26 | breqtrd | |
28 | simp31 | |
|
29 | simp32 | |
|
30 | simp33 | |
|
31 | 30 | necomd | |
32 | eqid | |
|
33 | 1 2 3 8 4 5 6 7 32 | cdlemh | |
34 | 12 11 15 27 28 29 31 33 | syl133anc | |
35 | 2 4 5 6 9 | ltrniotacl | |
36 | 10 11 34 35 | syl3anc | |