Step | Hyp | Ref
| Expression |
1 | | rexeq 2625 |
. . 3
|
2 | 1 | dcbid 823 |
. 2
DECID
DECID |
3 | | rexeq 2625 |
. . 3
|
4 | 3 | dcbid 823 |
. 2
DECID
DECID
|
5 | | rexeq 2625 |
. . 3
|
6 | 5 | dcbid 823 |
. 2
DECID DECID |
7 | | rexeq 2625 |
. . 3
|
8 | 7 | dcbid 823 |
. 2
DECID
DECID
|
9 | | rex0 3375 |
. . . . 5
|
10 | 9 | olci 721 |
. . . 4
|
11 | | df-dc 820 |
. . . 4
DECID
|
12 | 10, 11 | mpbir 145 |
. . 3
DECID |
13 | 12 | a1i 9 |
. 2
DECID DECID |
14 | | simpr 109 |
. . . . . . . . 9
DECID
DECID
|
15 | | sbsbc 2908 |
. . . . . . . . . 10
|
16 | | rexsns 3558 |
. . . . . . . . . 10
|
17 | 15, 16 | bitr4i 186 |
. . . . . . . . 9
|
18 | 14, 17 | sylib 121 |
. . . . . . . 8
DECID
DECID
|
19 | 18 | olcd 723 |
. . . . . . 7
DECID
DECID
|
20 | | rexun 3251 |
. . . . . . 7
|
21 | 19, 20 | sylibr 133 |
. . . . . 6
DECID
DECID
|
22 | 21 | orcd 722 |
. . . . 5
DECID
DECID
|
23 | | df-dc 820 |
. . . . 5
DECID |
24 | 22, 23 | sylibr 133 |
. . . 4
DECID
DECID
DECID |
25 | | simpr 109 |
. . . . . . . . 9
DECID
DECID
|
26 | 25 | orcd 722 |
. . . . . . . 8
DECID
DECID
|
27 | 26, 20 | sylibr 133 |
. . . . . . 7
DECID
DECID
|
28 | 27 | orcd 722 |
. . . . . 6
DECID
DECID
|
29 | 28, 23 | sylibr 133 |
. . . . 5
DECID
DECID
DECID
|
30 | | simpr 109 |
. . . . . . . . 9
DECID
DECID
|
31 | | simpr 109 |
. . . . . . . . . . 11
DECID
DECID
|
32 | 17 | notbii 657 |
. . . . . . . . . . 11
|
33 | 31, 32 | sylib 121 |
. . . . . . . . . 10
DECID
DECID
|
34 | 33 | adantr 274 |
. . . . . . . . 9
DECID
DECID
|
35 | | ioran 741 |
. . . . . . . . 9
|
36 | 30, 34, 35 | sylanbrc 413 |
. . . . . . . 8
DECID
DECID
|
37 | 20 | notbii 657 |
. . . . . . . 8
|
38 | 36, 37 | sylibr 133 |
. . . . . . 7
DECID
DECID
|
39 | 38 | olcd 723 |
. . . . . 6
DECID
DECID
|
40 | 39, 23 | sylibr 133 |
. . . . 5
DECID
DECID
DECID
|
41 | | exmiddc 821 |
. . . . . 6
DECID
|
42 | 41 | ad2antlr 480 |
. . . . 5
DECID
DECID
|
43 | 29, 40, 42 | mpjaodan 787 |
. . . 4
DECID
DECID
DECID |
44 | | simplrr 525 |
. . . . . . 7
DECID
DECID |
45 | 44 | eldifad 3077 |
. . . . . 6
DECID
DECID |
46 | | simp-4r 531 |
. . . . . 6
DECID
DECID
DECID |
47 | | nfs1v 1910 |
. . . . . . . 8
|
48 | 47 | nfdc 1637 |
. . . . . . 7
DECID |
49 | | sbequ12 1744 |
. . . . . . . 8
|
50 | 49 | dcbid 823 |
. . . . . . 7
DECID
DECID |
51 | 48, 50 | rspc 2778 |
. . . . . 6
DECID DECID |
52 | 45, 46, 51 | sylc 62 |
. . . . 5
DECID
DECID
DECID |
53 | | exmiddc 821 |
. . . . 5
DECID |
54 | 52, 53 | syl 14 |
. . . 4
DECID
DECID |
55 | 24, 43, 54 | mpjaodan 787 |
. . 3
DECID
DECID
DECID |
56 | 55 | ex 114 |
. 2
DECID
DECID DECID
|
57 | | simpl 108 |
. 2
DECID |
58 | 2, 4, 6, 8, 13, 56, 57 | findcard2sd 6779 |
1
DECID DECID |