Description: Part of proof of Lemma D in Crawley p. 113. The R =/= P requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemd3.l | |
|
cdlemd3.j | |
||
cdlemd3.a | |
||
cdlemd3.h | |
||
Assertion | cdlemd3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemd3.l | |
|
2 | cdlemd3.j | |
|
3 | cdlemd3.a | |
|
4 | cdlemd3.h | |
|
5 | simp33 | |
|
6 | simp1l | |
|
7 | simp31 | |
|
8 | simp32 | |
|
9 | simp21l | |
|
10 | simp233 | |
|
11 | 1 2 3 | hlatexch1 | |
12 | 6 7 8 9 10 11 | syl131anc | |
13 | simp22l | |
|
14 | 1 2 3 | hlatlej1 | |
15 | 6 9 13 14 | syl3anc | |
16 | simp232 | |
|
17 | 6 | hllatd | |
18 | eqid | |
|
19 | 18 3 | atbase | |
20 | 9 19 | syl | |
21 | 18 3 | atbase | |
22 | 7 21 | syl | |
23 | 18 3 | atbase | |
24 | 13 23 | syl | |
25 | 18 2 | latjcl | |
26 | 17 20 24 25 | syl3anc | |
27 | 18 1 2 | latjle12 | |
28 | 17 20 22 26 27 | syl13anc | |
29 | 15 16 28 | mpbi2and | |
30 | 18 3 | atbase | |
31 | 8 30 | syl | |
32 | 18 2 | latjcl | |
33 | 17 20 22 32 | syl3anc | |
34 | 18 1 | lattr | |
35 | 17 31 33 26 34 | syl13anc | |
36 | 29 35 | mpan2d | |
37 | 12 36 | syld | |
38 | 5 37 | mtod | |