Proof of Theorem reusv3
Step | Hyp | Ref
| Expression |
1 | | reusv3.1 |
. . . . 5
|
2 | | reusv3.2 |
. . . . . 6
|
3 | 2 | eleq1d 2686 |
. . . . 5
|
4 | 1, 3 | anbi12d 747 |
. . . 4
|
5 | 4 | cbvrexv 3172 |
. . 3
|
6 | | nfra2 2946 |
. . . . 5
|
7 | | nfv 1843 |
. . . . 5
|
8 | 6, 7 | nfim 1825 |
. . . 4
|
9 | | risset 3062 |
. . . . . 6
|
10 | | ralcom 3098 |
. . . . . . . . . . . . . 14
|
11 | | impexp 462 |
. . . . . . . . . . . . . . . . . 18
|
12 | | bi2.04 376 |
. . . . . . . . . . . . . . . . . 18
|
13 | 11, 12 | bitri 264 |
. . . . . . . . . . . . . . . . 17
|
14 | 13 | ralbii 2980 |
. . . . . . . . . . . . . . . 16
|
15 | | r19.21v 2960 |
. . . . . . . . . . . . . . . 16
|
16 | 14, 15 | bitri 264 |
. . . . . . . . . . . . . . 15
|
17 | 16 | ralbii 2980 |
. . . . . . . . . . . . . 14
|
18 | 10, 17 | bitri 264 |
. . . . . . . . . . . . 13
|
19 | | rsp 2929 |
. . . . . . . . . . . . 13
|
20 | 18, 19 | sylbi 207 |
. . . . . . . . . . . 12
|
21 | 20 | com3l 89 |
. . . . . . . . . . 11
|
22 | 21 | imp31 448 |
. . . . . . . . . 10
|
23 | | eqeq1 2626 |
. . . . . . . . . . . . 13
|
24 | | eqcom 2629 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | syl6bb 276 |
. . . . . . . . . . . 12
|
26 | 25 | imbi2d 330 |
. . . . . . . . . . 11
|
27 | 26 | ralbidv 2986 |
. . . . . . . . . 10
|
28 | 22, 27 | syl5ibrcom 237 |
. . . . . . . . 9
|
29 | 28 | reximdv 3016 |
. . . . . . . 8
|
30 | 29 | ex 450 |
. . . . . . 7
|
31 | 30 | com23 86 |
. . . . . 6
|
32 | 9, 31 | syl5bi 232 |
. . . . 5
|
33 | 32 | expimpd 629 |
. . . 4
|
34 | 8, 33 | rexlimi 3024 |
. . 3
|
35 | 5, 34 | sylbi 207 |
. 2
|
36 | 1, 2 | reusv3i 4875 |
. 2
|
37 | 35, 36 | impbid1 215 |
1
|