Description: TODO fix comment. (Contributed by NM, 29-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemefrs27.b | |
|
cdlemefrs27.l | |
||
cdlemefrs27.j | |
||
cdlemefrs27.m | |
||
cdlemefrs27.a | |
||
cdlemefrs27.h | |
||
cdlemefrs27.eq | |
||
cdlemefrs27.nb | |
||
Assertion | cdlemefrs29bpre0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemefrs27.b | |
|
2 | cdlemefrs27.l | |
|
3 | cdlemefrs27.j | |
|
4 | cdlemefrs27.m | |
|
5 | cdlemefrs27.a | |
|
6 | cdlemefrs27.h | |
|
7 | cdlemefrs27.eq | |
|
8 | cdlemefrs27.nb | |
|
9 | df-ral | |
|
10 | anass | |
|
11 | 10 | imbi1i | |
12 | impexp | |
|
13 | impexp | |
|
14 | 11 12 13 | 3bitr3ri | |
15 | simpl11 | |
|
16 | simpl2r | |
|
17 | eqid | |
|
18 | 2 4 17 5 6 | lhpmat | |
19 | 15 16 18 | syl2anc | |
20 | 19 | oveq2d | |
21 | simp11l | |
|
22 | hlol | |
|
23 | 21 22 | syl | |
24 | 23 | adantr | |
25 | simprl | |
|
26 | 1 5 | atbase | |
27 | 25 26 | syl | |
28 | 1 3 17 | olj01 | |
29 | 24 27 28 | syl2anc | |
30 | 20 29 | eqtrd | |
31 | 30 | eqeq1d | |
32 | 19 | oveq2d | |
33 | simpl1 | |
|
34 | simpl2l | |
|
35 | simprr | |
|
36 | 33 34 25 35 8 | syl112anc | |
37 | 1 3 17 | olj01 | |
38 | 24 36 37 | syl2anc | |
39 | 32 38 | eqtrd | |
40 | 39 | eqeq2d | |
41 | 31 40 | imbi12d | |
42 | 41 | pm5.74da | |
43 | impexp | |
|
44 | simp2rl | |
|
45 | simp2rr | |
|
46 | simp3 | |
|
47 | eleq1 | |
|
48 | breq1 | |
|
49 | 48 | notbid | |
50 | 49 7 | anbi12d | |
51 | 47 50 | anbi12d | |
52 | 51 | biimprcd | |
53 | 44 45 46 52 | syl12anc | |
54 | 53 | pm4.71rd | |
55 | 54 | imbi1d | |
56 | eqcom | |
|
57 | 56 | imbi2i | |
58 | 55 57 | bitr3di | |
59 | 43 58 | bitr3id | |
60 | 42 59 | bitrd | |
61 | 14 60 | syl5bb | |
62 | 61 | albidv | |
63 | 9 62 | syl5bb | |
64 | nfcv | |
|
65 | 64 | csbiebg | |
66 | 44 65 | syl | |
67 | eqcom | |
|
68 | 66 67 | bitrdi | |
69 | 63 68 | bitrd | |