Description: Part of proof of Lemma K of Crawley p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 ? (Contributed by NM, 19-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemk4.b | |
|
cdlemk4.l | |
||
cdlemk4.j | |
||
cdlemk4.m | |
||
cdlemk4.a | |
||
cdlemk4.h | |
||
cdlemk4.t | |
||
cdlemk4.r | |
||
cdlemk4.z | |
||
cdlemk4.y | |
||
cdlemk4.x | |
||
Assertion | cdlemk38 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemk4.b | |
|
2 | cdlemk4.l | |
|
3 | cdlemk4.j | |
|
4 | cdlemk4.m | |
|
5 | cdlemk4.a | |
|
6 | cdlemk4.h | |
|
7 | cdlemk4.t | |
|
8 | cdlemk4.r | |
|
9 | cdlemk4.z | |
|
10 | cdlemk4.y | |
|
11 | cdlemk4.x | |
|
12 | 1 6 7 8 | cdlemftr2 | |
13 | 12 | 3ad2ant1 | |
14 | nfv | |
|
15 | nfra1 | |
|
16 | nfcv | |
|
17 | 15 16 | nfriota | |
18 | 11 17 | nfcxfr | |
19 | nfcv | |
|
20 | 18 19 | nffv | |
21 | nfcv | |
|
22 | nfcv | |
|
23 | 20 21 22 | nfbr | |
24 | simpl1 | |
|
25 | simpl21 | |
|
26 | simpl22 | |
|
27 | simpl23 | |
|
28 | simpl3l | |
|
29 | simpl3r | |
|
30 | simpr | |
|
31 | 1 2 3 4 5 6 7 8 9 10 11 | cdlemk37 | |
32 | 24 25 26 27 28 29 30 31 | syl331anc | |
33 | 32 | exp32 | |
34 | 14 23 33 | rexlimd | |
35 | 13 34 | mpd | |