Description: Part of proof of Lemma K of Crawley p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemk5.b | |
|
cdlemk5.l | |
||
cdlemk5.j | |
||
cdlemk5.m | |
||
cdlemk5.a | |
||
cdlemk5.h | |
||
cdlemk5.t | |
||
cdlemk5.r | |
||
cdlemk5.z | |
||
cdlemk5.y | |
||
cdlemk5.x | |
||
Assertion | cdlemk42 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemk5.b | |
|
2 | cdlemk5.l | |
|
3 | cdlemk5.j | |
|
4 | cdlemk5.m | |
|
5 | cdlemk5.a | |
|
6 | cdlemk5.h | |
|
7 | cdlemk5.t | |
|
8 | cdlemk5.r | |
|
9 | cdlemk5.z | |
|
10 | cdlemk5.y | |
|
11 | cdlemk5.x | |
|
12 | simp13l | |
|
13 | 1 2 3 4 5 6 7 8 9 10 11 | cdlemk36 | |
14 | 13 | sbcth | |
15 | sbcimg | |
|
16 | 14 15 | mpbid | |
17 | eleq1 | |
|
18 | neeq1 | |
|
19 | 17 18 | anbi12d | |
20 | 19 | 3anbi3d | |
21 | fveq2 | |
|
22 | 21 | neeq2d | |
23 | 22 | 3anbi3d | |
24 | 23 | anbi2d | |
25 | 20 24 | 3anbi13d | |
26 | 25 | sbcieg | |
27 | sbceqg | |
|
28 | csbfv12 | |
|
29 | csbconstg | |
|
30 | 29 | fveq2d | |
31 | 28 30 | eqtrid | |
32 | 31 | eqeq1d | |
33 | 27 32 | bitrd | |
34 | 16 26 33 | 3imtr3d | |
35 | 12 34 | mpcom | |