Description: Part of proof of Lemma C in Crawley p. 112. (Contributed by NM, 25-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemc2.l | |
|
cdlemc2.j | |
||
cdlemc2.m | |
||
cdlemc2.a | |
||
cdlemc2.h | |
||
cdlemc2.t | |
||
Assertion | cdlemc2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemc2.l | |
|
2 | cdlemc2.j | |
|
3 | cdlemc2.m | |
|
4 | cdlemc2.a | |
|
5 | cdlemc2.h | |
|
6 | cdlemc2.t | |
|
7 | simp1l | |
|
8 | simp3ll | |
|
9 | simp3rl | |
|
10 | 1 2 4 | hlatlej2 | |
11 | 7 8 9 10 | syl3anc | |
12 | simp1 | |
|
13 | eqid | |
|
14 | 13 4 | atbase | |
15 | 9 14 | syl | |
16 | simp3l | |
|
17 | 13 1 2 3 4 5 | cdlemc1 | |
18 | 12 15 16 17 | syl3anc | |
19 | 11 18 | breqtrrd | |
20 | simp2 | |
|
21 | 7 | hllatd | |
22 | 13 4 | atbase | |
23 | 8 22 | syl | |
24 | 13 2 | latjcl | |
25 | 21 23 15 24 | syl3anc | |
26 | simp1r | |
|
27 | 13 5 | lhpbase | |
28 | 26 27 | syl | |
29 | 13 3 | latmcl | |
30 | 21 25 28 29 | syl3anc | |
31 | 13 2 | latjcl | |
32 | 21 23 30 31 | syl3anc | |
33 | 13 1 5 6 | ltrnle | |
34 | 12 20 15 32 33 | syl112anc | |
35 | 19 34 | mpbid | |
36 | 13 2 5 6 | ltrnj | |
37 | 12 20 23 30 36 | syl112anc | |
38 | 13 1 3 | latmle2 | |
39 | 21 25 28 38 | syl3anc | |
40 | 13 1 5 6 | ltrnval1 | |
41 | 12 20 30 39 40 | syl112anc | |
42 | 41 | oveq2d | |
43 | 37 42 | eqtrd | |
44 | 35 43 | breqtrd | |