Step | Hyp | Ref
| Expression |
1 | | 4cycl2v2nb 27153 |
. 2
|
2 | | preq2 4269 |
. . . . . . . . . . . . . . . 16
|
3 | | preq1 4268 |
. . . . . . . . . . . . . . . 16
|
4 | 2, 3 | preq12d 4276 |
. . . . . . . . . . . . . . 15
|
5 | 4 | sseq1d 3632 |
. . . . . . . . . . . . . 14
|
6 | 5 | anbi1d 741 |
. . . . . . . . . . . . 13
|
7 | | neeq1 2856 |
. . . . . . . . . . . . 13
|
8 | 6, 7 | anbi12d 747 |
. . . . . . . . . . . 12
|
9 | | preq2 4269 |
. . . . . . . . . . . . . . . 16
|
10 | | preq1 4268 |
. . . . . . . . . . . . . . . 16
|
11 | 9, 10 | preq12d 4276 |
. . . . . . . . . . . . . . 15
|
12 | 11 | sseq1d 3632 |
. . . . . . . . . . . . . 14
|
13 | 12 | anbi2d 740 |
. . . . . . . . . . . . 13
|
14 | | neeq2 2857 |
. . . . . . . . . . . . 13
|
15 | 13, 14 | anbi12d 747 |
. . . . . . . . . . . 12
|
16 | 8, 15 | rspc2ev 3324 |
. . . . . . . . . . 11
|
17 | 16 | 3expa 1265 |
. . . . . . . . . 10
|
18 | 17 | expcom 451 |
. . . . . . . . 9
|
19 | 18 | ex 450 |
. . . . . . . 8
|
20 | 19 | com13 88 |
. . . . . . 7
|
21 | 20 | 3impia 1261 |
. . . . . 6
|
22 | 21 | impcom 446 |
. . . . 5
|
23 | | rexnal 2995 |
. . . . . 6
|
24 | | rexnal 2995 |
. . . . . . . 8
|
25 | | annim 441 |
. . . . . . . . . 10
|
26 | | df-ne 2795 |
. . . . . . . . . . . 12
|
27 | 26 | bicomi 214 |
. . . . . . . . . . 11
|
28 | 27 | anbi2i 730 |
. . . . . . . . . 10
|
29 | 25, 28 | bitr3i 266 |
. . . . . . . . 9
|
30 | 29 | rexbii 3041 |
. . . . . . . 8
|
31 | 24, 30 | bitr3i 266 |
. . . . . . 7
|
32 | 31 | rexbii 3041 |
. . . . . 6
|
33 | 23, 32 | bitr3i 266 |
. . . . 5
|
34 | 22, 33 | sylibr 224 |
. . . 4
|
35 | 34 | intnand 962 |
. . 3
|
36 | | preq2 4269 |
. . . . . 6
|
37 | | preq1 4268 |
. . . . . 6
|
38 | 36, 37 | preq12d 4276 |
. . . . 5
|
39 | 38 | sseq1d 3632 |
. . . 4
|
40 | 39 | reu4 3400 |
. . 3
|
41 | 35, 40 | sylnibr 319 |
. 2
|
42 | 1, 41 | stoic3 1701 |
1
|