Description: Part of proof of Lemma E in Crawley p. 113. Show that f(r) is for on and off P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 19-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 | cdleme41sn4aw | |
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 | simp23 | |
|
16 | simp22 | |
|
17 | simp32 | |
|
18 | simp31 | |
|
19 | simp33 | |
|
20 | 19 | necomd | |
21 | 1 2 3 4 5 6 7 8 9 10 11 12 | cdleme41sn3aw | |
22 | 13 14 15 16 17 18 20 21 | syl133anc | |
23 | 22 | necomd | |