Proof of Theorem ntrneikb
Step | Hyp | Ref
| Expression |
1 | | con34b 306 |
. . . . . . 7
|
2 | 1 | albii 1747 |
. . . . . 6
|
3 | | 19.21v 1868 |
. . . . . 6
|
4 | | nne 2798 |
. . . . . . 7
|
5 | | elin 3796 |
. . . . . . . . . . 11
|
6 | 5 | imbi1i 339 |
. . . . . . . . . 10
|
7 | | noel 3919 |
. . . . . . . . . . 11
|
8 | | imnot 355 |
. . . . . . . . . . 11
|
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
|
10 | 6, 9 | bitr2i 265 |
. . . . . . . . 9
|
11 | 10 | albii 1747 |
. . . . . . . 8
|
12 | | dfss2 3591 |
. . . . . . . 8
|
13 | | ss0b 3973 |
. . . . . . . 8
|
14 | 11, 12, 13 | 3bitr2i 288 |
. . . . . . 7
|
15 | 4, 14 | imbi12i 340 |
. . . . . 6
|
16 | 2, 3, 15 | 3bitrri 287 |
. . . . 5
|
17 | | ntrnei.o |
. . . . . . . . . . . . . . . . . . 19
|
18 | | ntrnei.f |
. . . . . . . . . . . . . . . . . . 19
|
19 | | ntrnei.r |
. . . . . . . . . . . . . . . . . . 19
|
20 | 17, 18, 19 | ntrneiiex 38374 |
. . . . . . . . . . . . . . . . . 18
|
21 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
|
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
23 | 22 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
|
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . 15
|
25 | 24 | elpwid 4170 |
. . . . . . . . . . . . . 14
|
26 | 25 | sseld 3602 |
. . . . . . . . . . . . 13
|
27 | 26 | adantrd 484 |
. . . . . . . . . . . 12
|
28 | 27 | imp 445 |
. . . . . . . . . . 11
|
29 | | biimt 350 |
. . . . . . . . . . 11
|
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
|
31 | 30 | pm5.74da 723 |
. . . . . . . . 9
|
32 | | bi2.04 376 |
. . . . . . . . 9
|
33 | 31, 32 | syl6bb 276 |
. . . . . . . 8
|
34 | 33 | albidv 1849 |
. . . . . . 7
|
35 | | df-ral 2917 |
. . . . . . 7
|
36 | 34, 35 | syl6bbr 278 |
. . . . . 6
|
37 | 19 | ad3antrrr 766 |
. . . . . . . . . 10
|
38 | | simpr 477 |
. . . . . . . . . 10
|
39 | | simpllr 799 |
. . . . . . . . . 10
|
40 | 17, 18, 37, 38, 39 | ntrneiel 38379 |
. . . . . . . . 9
|
41 | | simplr 792 |
. . . . . . . . . 10
|
42 | 17, 18, 37, 38, 41 | ntrneiel 38379 |
. . . . . . . . 9
|
43 | 40, 42 | anbi12d 747 |
. . . . . . . 8
|
44 | 43 | imbi1d 331 |
. . . . . . 7
|
45 | 44 | ralbidva 2985 |
. . . . . 6
|
46 | 36, 45 | bitrd 268 |
. . . . 5
|
47 | 16, 46 | syl5bb 272 |
. . . 4
|
48 | 47 | ralbidva 2985 |
. . 3
|
49 | 48 | ralbidva 2985 |
. 2
|
50 | | alrot3 2038 |
. . . 4
|
51 | | 3anrot 1043 |
. . . . . . 7
|
52 | 51 | imbi1i 339 |
. . . . . 6
|
53 | 52 | albii 1747 |
. . . . 5
|
54 | 53 | 2albii 1748 |
. . . 4
|
55 | 50, 54 | bitr2i 265 |
. . 3
|
56 | | r3al 2940 |
. . 3
|
57 | | r3al 2940 |
. . 3
|
58 | 55, 56, 57 | 3bitr4i 292 |
. 2
|
59 | 49, 58 | syl6bb 276 |
1
|