Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 14-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme11.l | |
|
cdleme11.j | |
||
cdleme11.m | |
||
cdleme11.a | |
||
cdleme11.h | |
||
cdleme11.u | |
||
cdleme11.c | |
||
cdleme11.d | |
||
cdleme11.f | |
||
Assertion | cdleme11j | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme11.l | |
|
2 | cdleme11.j | |
|
3 | cdleme11.m | |
|
4 | cdleme11.a | |
|
5 | cdleme11.h | |
|
6 | cdleme11.u | |
|
7 | cdleme11.c | |
|
8 | cdleme11.d | |
|
9 | cdleme11.f | |
|
10 | simp1l | |
|
11 | simp22l | |
|
12 | 1 2 3 4 5 6 9 | cdleme3fa | |
13 | 1 2 4 | hlatlej2 | |
14 | 10 11 12 13 | syl3anc | |
15 | simp1 | |
|
16 | simp21l | |
|
17 | simp22 | |
|
18 | simp23l | |
|
19 | simp3l | |
|
20 | 1 2 3 4 5 6 7 6 9 | cdleme11g | |
21 | 15 16 17 18 19 20 | syl131anc | |
22 | 14 21 | breqtrd | |
23 | simp21 | |
|
24 | simp3r | |
|
25 | 1 2 3 4 | cdleme00a | |
26 | 10 16 11 18 24 25 | syl131anc | |
27 | 26 | necomd | |
28 | 1 2 3 4 5 7 | cdleme9a | |
29 | 15 23 18 27 28 | syl112anc | |
30 | simp3 | |
|
31 | 1 2 3 4 5 6 7 6 9 | cdleme11h | |
32 | 15 23 17 18 30 31 | syl131anc | |
33 | 1 2 4 | hlatexch1 | |
34 | 10 12 29 11 32 33 | syl131anc | |
35 | 22 34 | mpd | |