Proof of Theorem cdlemefrs29bpre0
Step | Hyp | Ref
| Expression |
1 | | df-ral 2917 |
. . 3
|
2 | | anass 681 |
. . . . . . 7
|
3 | 2 | imbi1i 339 |
. . . . . 6
|
4 | | impexp 462 |
. . . . . 6
|
5 | | impexp 462 |
. . . . . 6
|
6 | 3, 4, 5 | 3bitr3ri 291 |
. . . . 5
|
7 | | simpl11 1136 |
. . . . . . . . . . . 12
|
8 | | simpl2r 1115 |
. . . . . . . . . . . 12
|
9 | | cdlemefrs27.l |
. . . . . . . . . . . . 13
|
10 | | cdlemefrs27.m |
. . . . . . . . . . . . 13
|
11 | | eqid 2622 |
. . . . . . . . . . . . 13
|
12 | | cdlemefrs27.a |
. . . . . . . . . . . . 13
|
13 | | cdlemefrs27.h |
. . . . . . . . . . . . 13
|
14 | 9, 10, 11, 12, 13 | lhpmat 35316 |
. . . . . . . . . . . 12
|
15 | 7, 8, 14 | syl2anc 693 |
. . . . . . . . . . 11
|
16 | 15 | oveq2d 6666 |
. . . . . . . . . 10
|
17 | | simp11l 1172 |
. . . . . . . . . . . . 13
|
18 | | hlol 34648 |
. . . . . . . . . . . . 13
|
19 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
|
20 | 19 | adantr 481 |
. . . . . . . . . . 11
|
21 | | simprl 794 |
. . . . . . . . . . . 12
|
22 | | cdlemefrs27.b |
. . . . . . . . . . . . 13
|
23 | 22, 12 | atbase 34576 |
. . . . . . . . . . . 12
|
24 | 21, 23 | syl 17 |
. . . . . . . . . . 11
|
25 | | cdlemefrs27.j |
. . . . . . . . . . . 12
|
26 | 22, 25, 11 | olj01 34512 |
. . . . . . . . . . 11
|
27 | 20, 24, 26 | syl2anc 693 |
. . . . . . . . . 10
|
28 | 16, 27 | eqtrd 2656 |
. . . . . . . . 9
|
29 | 28 | eqeq1d 2624 |
. . . . . . . 8
|
30 | 15 | oveq2d 6666 |
. . . . . . . . . 10
|
31 | | simpl1 1064 |
. . . . . . . . . . . 12
|
32 | | simpl2l 1114 |
. . . . . . . . . . . 12
|
33 | | simprr 796 |
. . . . . . . . . . . 12
|
34 | | cdlemefrs27.nb |
. . . . . . . . . . . 12
|
35 | 31, 32, 21, 33, 34 | syl112anc 1330 |
. . . . . . . . . . 11
|
36 | 22, 25, 11 | olj01 34512 |
. . . . . . . . . . 11
|
37 | 20, 35, 36 | syl2anc 693 |
. . . . . . . . . 10
|
38 | 30, 37 | eqtrd 2656 |
. . . . . . . . 9
|
39 | 38 | eqeq2d 2632 |
. . . . . . . 8
|
40 | 29, 39 | imbi12d 334 |
. . . . . . 7
|
41 | 40 | pm5.74da 723 |
. . . . . 6
|
42 | | impexp 462 |
. . . . . . 7
|
43 | | eqcom 2629 |
. . . . . . . . 9
|
44 | 43 | imbi2i 326 |
. . . . . . . 8
|
45 | | simp2rl 1130 |
. . . . . . . . . . 11
|
46 | | simp2rr 1131 |
. . . . . . . . . . 11
|
47 | | simp3 1063 |
. . . . . . . . . . 11
|
48 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
49 | | breq1 4656 |
. . . . . . . . . . . . . . 15
|
50 | 49 | notbid 308 |
. . . . . . . . . . . . . 14
|
51 | | cdlemefrs27.eq |
. . . . . . . . . . . . . 14
|
52 | 50, 51 | anbi12d 747 |
. . . . . . . . . . . . 13
|
53 | 48, 52 | anbi12d 747 |
. . . . . . . . . . . 12
|
54 | 53 | biimprcd 240 |
. . . . . . . . . . 11
|
55 | 45, 46, 47, 54 | syl12anc 1324 |
. . . . . . . . . 10
|
56 | 55 | pm4.71rd 667 |
. . . . . . . . 9
|
57 | 56 | imbi1d 331 |
. . . . . . . 8
|
58 | 44, 57 | syl5rbbr 275 |
. . . . . . 7
|
59 | 42, 58 | syl5bbr 274 |
. . . . . 6
|
60 | 41, 59 | bitrd 268 |
. . . . 5
|
61 | 6, 60 | syl5bb 272 |
. . . 4
|
62 | 61 | albidv 1849 |
. . 3
|
63 | 1, 62 | syl5bb 272 |
. 2
|
64 | | nfcv 2764 |
. . . . 5
|
65 | 64 | csbiebg 3556 |
. . . 4
|
66 | 45, 65 | syl 17 |
. . 3
|
67 | | eqcom 2629 |
. . 3
|
68 | 66, 67 | syl6bb 276 |
. 2
|
69 | 63, 68 | bitrd 268 |
1
|