Description: Part of proof of Lemma E in Crawley p. 113. Eliminate the s =/= t antecedent in cdleme27a . (Contributed by NM, 3-Feb-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme26.b | |
|
cdleme26.l | |
||
cdleme26.j | |
||
cdleme26.m | |
||
cdleme26.a | |
||
cdleme26.h | |
||
cdleme27.u | |
||
cdleme27.f | |
||
cdleme27.z | |
||
cdleme27.n | |
||
cdleme27.d | |
||
cdleme27.c | |
||
cdleme27.g | |
||
cdleme27.o | |
||
cdleme27.e | |
||
cdleme27.y | |
||
Assertion | cdleme27N | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme26.b | |
|
2 | cdleme26.l | |
|
3 | cdleme26.j | |
|
4 | cdleme26.m | |
|
5 | cdleme26.a | |
|
6 | cdleme26.h | |
|
7 | cdleme27.u | |
|
8 | cdleme27.f | |
|
9 | cdleme27.z | |
|
10 | cdleme27.n | |
|
11 | cdleme27.d | |
|
12 | cdleme27.c | |
|
13 | cdleme27.g | |
|
14 | cdleme27.o | |
|
15 | cdleme27.e | |
|
16 | cdleme27.y | |
|
17 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | cdleme27b | |
18 | 17 | adantl | |
19 | simp11l | |
|
20 | 19 | hllatd | |
21 | simp11r | |
|
22 | simp21 | |
|
23 | simp22 | |
|
24 | simp23 | |
|
25 | simp12 | |
|
26 | 1 2 3 4 5 6 7 13 9 14 15 16 | cdleme27cl | |
27 | 19 21 22 23 24 25 26 | syl222anc | |
28 | simp3rl | |
|
29 | 1 5 | atbase | |
30 | 28 29 | syl | |
31 | 1 2 3 | latlej1 | |
32 | 20 27 30 31 | syl3anc | |
33 | 32 | adantr | |
34 | 18 33 | eqbrtrd | |
35 | simpl11 | |
|
36 | simpl12 | |
|
37 | simpl13 | |
|
38 | simpl21 | |
|
39 | simpl22 | |
|
40 | simpl23 | |
|
41 | simpr | |
|
42 | simpl3l | |
|
43 | 41 42 | jca | |
44 | simpl3r | |
|
45 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | cdleme27a | |
46 | 35 36 37 38 39 40 43 44 45 | syl332anc | |
47 | 34 46 | pm2.61dane | |