Description: Part of proof of Lemma E in Crawley p. 113. Show that f(r) is different on and off the P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme41.b | |
|
cdleme41.l | |
||
cdleme41.j | |
||
cdleme41.m | |
||
cdleme41.a | |
||
cdleme41.h | |
||
cdleme41.u | |
||
cdleme41.d | |
||
cdleme41.e | |
||
cdleme41.g | |
||
cdleme41.i | |
||
cdleme41.n | |
||
Assertion | cdleme41sn3aw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme41.b | |
|
2 | cdleme41.l | |
|
3 | cdleme41.j | |
|
4 | cdleme41.m | |
|
5 | cdleme41.a | |
|
6 | cdleme41.h | |
|
7 | cdleme41.u | |
|
8 | cdleme41.d | |
|
9 | cdleme41.e | |
|
10 | cdleme41.g | |
|
11 | cdleme41.i | |
|
12 | cdleme41.n | |
|
13 | simp1 | |
|
14 | simp21 | |
|
15 | simp22 | |
|
16 | simp31 | |
|
17 | eqid | |
|
18 | eqid | |
|
19 | 1 2 3 4 5 6 7 8 9 10 11 12 17 18 | cdleme41sn3a | |
20 | 13 14 15 16 19 | syl121anc | |
21 | simp23 | |
|
22 | simp32 | |
|
23 | 1 2 3 4 5 6 7 8 12 | cdleme35sn3a | |
24 | 13 14 21 22 23 | syl121anc | |
25 | nbrne2 | |
|
26 | 20 24 25 | syl2anc | |