Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 1-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemd4.l | |
|
cdlemd4.j | |
||
cdlemd4.a | |
||
cdlemd4.h | |
||
cdlemd4.t | |
||
Assertion | cdlemd7 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemd4.l | |
|
2 | cdlemd4.j | |
|
3 | cdlemd4.a | |
|
4 | cdlemd4.h | |
|
5 | cdlemd4.t | |
|
6 | simp1 | |
|
7 | simp2l | |
|
8 | simp2r | |
|
9 | simp11l | |
|
10 | 9 | hllatd | |
11 | simp2rl | |
|
12 | eqid | |
|
13 | 12 3 | atbase | |
14 | 11 13 | syl | |
15 | simp2ll | |
|
16 | 12 3 | atbase | |
17 | 15 16 | syl | |
18 | simp11 | |
|
19 | simp12l | |
|
20 | 12 4 5 | ltrncl | |
21 | 18 19 17 20 | syl3anc | |
22 | simp3r | |
|
23 | 12 1 2 | latnlej1l | |
24 | 23 | necomd | |
25 | 10 14 17 21 22 24 | syl131anc | |
26 | simp3l | |
|
27 | simp12 | |
|
28 | 1 2 3 4 5 | cdlemd6 | |
29 | 18 27 7 8 22 26 28 | syl231anc | |
30 | 1 2 3 4 5 | cdlemd5 | |
31 | 6 7 8 25 26 29 30 | syl132anc | |