Step | Hyp | Ref
| Expression |
1 | | breq2 4657 |
. . . . . . . 8
|
2 | 1 | cbvexvw 1970 |
. . . . . . 7
|
3 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
4 | 3 | anbi1d 741 |
. . . . . . . . . . . . 13
|
5 | | bianir 1009 |
. . . . . . . . . . . . . . . . . 18
|
6 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
7 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . 21
|
8 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . . . 21
|
9 | 7, 8 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
|
10 | 6, 9 | spcev 3300 |
. . . . . . . . . . . . . . . . . . 19
|
11 | 10 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
12 | 5, 11 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
13 | 12 | ex 450 |
. . . . . . . . . . . . . . . 16
|
14 | 13 | pm2.43a 54 |
. . . . . . . . . . . . . . 15
|
15 | 14 | adantld 483 |
. . . . . . . . . . . . . 14
|
16 | | nne 2798 |
. . . . . . . . . . . . . . . 16
|
17 | | notbi 309 |
. . . . . . . . . . . . . . . . . . . 20
|
18 | | bianir 1009 |
. . . . . . . . . . . . . . . . . . . . . 22
|
19 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
20 | 19 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
21 | | pm2.24 121 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
22 | 20, 21 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
23 | 22 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . 22
|
24 | 18, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
25 | 24 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | 17, 25 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 26 | com13 88 |
. . . . . . . . . . . . . . . . . 18
|
28 | 27 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
29 | 28 | com13 88 |
. . . . . . . . . . . . . . . 16
|
30 | 16, 29 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
31 | 30 | pm2.43i 52 |
. . . . . . . . . . . . . 14
|
32 | 15, 31 | pm2.61i 176 |
. . . . . . . . . . . . 13
|
33 | 4, 32 | syl6bi 243 |
. . . . . . . . . . . 12
|
34 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
35 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
|
36 | | neeq1 2856 |
. . . . . . . . . . . . . . . . 17
|
37 | 35, 36 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
38 | 34, 37 | spcev 3300 |
. . . . . . . . . . . . . . 15
|
39 | 38 | ex 450 |
. . . . . . . . . . . . . 14
|
40 | 39 | adantr 481 |
. . . . . . . . . . . . 13
|
41 | 40 | com12 32 |
. . . . . . . . . . . 12
|
42 | 33, 41 | pm2.61ine 2877 |
. . . . . . . . . . 11
|
43 | 42 | expcom 451 |
. . . . . . . . . 10
|
44 | 43 | exlimiv 1858 |
. . . . . . . . 9
|
45 | 44 | com12 32 |
. . . . . . . 8
|
46 | 45 | exlimiv 1858 |
. . . . . . 7
|
47 | 2, 46 | sylbi 207 |
. . . . . 6
|
48 | 47 | imp 445 |
. . . . 5
|
49 | 48 | a1i 11 |
. . . 4
|
50 | 49 | ss2abdv 3675 |
. . 3
|
51 | | suppvalbr 7299 |
. . 3
supp |
52 | | cnvimadfsn 7304 |
. . . 4
|
53 | 52 | a1i 11 |
. . 3
|
54 | 50, 51, 53 | 3sstr4d 3648 |
. 2
supp |
55 | | suppimacnvss 7305 |
. 2
supp |
56 | 54, 55 | eqssd 3620 |
1
supp |