Description: Part of proof of Lemma C in Crawley p. 113. (Contributed by NM, 26-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemc3.l | |
|
cdlemc3.j | |
||
cdlemc3.m | |
||
cdlemc3.a | |
||
cdlemc3.h | |
||
cdlemc3.t | |
||
cdlemc3.r | |
||
Assertion | cdlemc3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemc3.l | |
|
2 | cdlemc3.j | |
|
3 | cdlemc3.m | |
|
4 | cdlemc3.a | |
|
5 | cdlemc3.h | |
|
6 | cdlemc3.t | |
|
7 | cdlemc3.r | |
|
8 | simpll | |
|
9 | simpl | |
|
10 | simpr1 | |
|
11 | simpr2l | |
|
12 | 1 4 5 6 | ltrnat | |
13 | 9 10 11 12 | syl3anc | |
14 | simpr3l | |
|
15 | eqid | |
|
16 | 15 5 6 7 | trlcl | |
17 | 10 16 | syldan | |
18 | 1 4 5 6 | ltrnel | |
19 | 18 | 3adant3r3 | |
20 | 1 4 5 6 7 | trlnle | |
21 | 9 10 19 20 | syl3anc | |
22 | 15 1 2 4 | hlexch2 | |
23 | 8 13 14 17 21 22 | syl131anc | |
24 | 1 2 4 5 6 7 | trljat2 | |
25 | 24 | 3adant3r3 | |
26 | 25 | breq2d | |
27 | 23 26 | sylibd | |