Step | Hyp | Ref
| Expression |
1 | | a9e 1626 |
. 2
|
2 | | dveeq2or 1737 |
. . . . . 6
|
3 | | nfnf1 1476 |
. . . . . . . . . . 11
|
4 | 3 | nfri 1452 |
. . . . . . . . . 10
|
5 | | ax11v 1748 |
. . . . . . . . . . . . 13
|
6 | | equequ2 1639 |
. . . . . . . . . . . . . . 15
|
7 | 6 | adantl 271 |
. . . . . . . . . . . . . 14
|
8 | | nfr 1451 |
. . . . . . . . . . . . . . . . 17
|
9 | 8 | imp 122 |
. . . . . . . . . . . . . . . 16
|
10 | | hba1 1473 |
. . . . . . . . . . . . . . . . 17
|
11 | 6 | imbi1d 229 |
. . . . . . . . . . . . . . . . . 18
|
12 | 11 | sps 1470 |
. . . . . . . . . . . . . . . . 17
|
13 | 10, 12 | albidh 1409 |
. . . . . . . . . . . . . . . 16
|
14 | 9, 13 | syl 14 |
. . . . . . . . . . . . . . 15
|
15 | 14 | imbi2d 228 |
. . . . . . . . . . . . . 14
|
16 | 7, 15 | imbi12d 232 |
. . . . . . . . . . . . 13
|
17 | 5, 16 | mpbii 146 |
. . . . . . . . . . . 12
|
18 | 17 | ex 113 |
. . . . . . . . . . 11
|
19 | 18 | imp4a 341 |
. . . . . . . . . 10
|
20 | 4, 19 | alrimih 1398 |
. . . . . . . . 9
|
21 | | 19.21t 1514 |
. . . . . . . . 9
|
22 | 20, 21 | mpbid 145 |
. . . . . . . 8
|
23 | | hba1 1473 |
. . . . . . . . 9
|
24 | 23 | 19.23h 1427 |
. . . . . . . 8
|
25 | 22, 24 | syl6ib 159 |
. . . . . . 7
|
26 | 25 | orim2i 710 |
. . . . . 6
|
27 | 2, 26 | ax-mp 7 |
. . . . 5
|
28 | | pm2.76 754 |
. . . . 5
|
29 | 27, 28 | ax-mp 7 |
. . . 4
|
30 | 29 | olcs 687 |
. . 3
|
31 | 30 | exlimiv 1529 |
. 2
|
32 | 1, 31 | ax-mp 7 |
1
|