Step | Hyp | Ref
| Expression |
1 | | idn3 38840 |
. . . . . . . . . . . . . 14
|
2 | | simpr 477 |
. . . . . . . . . . . . . 14
|
3 | 1, 2 | e3 38964 |
. . . . . . . . . . . . 13
|
4 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
5 | 4 | sseli 3599 |
. . . . . . . . . . . . 13
|
6 | 3, 5 | e3 38964 |
. . . . . . . . . . . 12
|
7 | | inss1 3833 |
. . . . . . . . . . . . . . 15
|
8 | 7 | sseli 3599 |
. . . . . . . . . . . . . 14
|
9 | 3, 8 | e3 38964 |
. . . . . . . . . . . . 13
|
10 | | idn2 38838 |
. . . . . . . . . . . . . . . . . 18
|
11 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
12 | 10, 11 | e2 38856 |
. . . . . . . . . . . . . . . . 17
|
13 | | idn1 38790 |
. . . . . . . . . . . . . . . . . 18
|
14 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
15 | 13, 14 | e1a 38852 |
. . . . . . . . . . . . . . . . 17
|
16 | | ssel 3597 |
. . . . . . . . . . . . . . . . . 18
|
17 | 16 | com12 32 |
. . . . . . . . . . . . . . . . 17
|
18 | 12, 15, 17 | e21 38957 |
. . . . . . . . . . . . . . . 16
|
19 | | eloni 5733 |
. . . . . . . . . . . . . . . 16
|
20 | 18, 19 | e2 38856 |
. . . . . . . . . . . . . . 15
|
21 | | ordtr 5737 |
. . . . . . . . . . . . . . 15
|
22 | 20, 21 | e2 38856 |
. . . . . . . . . . . . . 14
|
23 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
24 | 1, 23 | e3 38964 |
. . . . . . . . . . . . . . 15
|
25 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
|
26 | 25 | sseli 3599 |
. . . . . . . . . . . . . . 15
|
27 | 24, 26 | e3 38964 |
. . . . . . . . . . . . . 14
|
28 | | trel 4759 |
. . . . . . . . . . . . . . 15
|
29 | 28 | expcomd 454 |
. . . . . . . . . . . . . 14
|
30 | 22, 27, 6, 29 | e233 38992 |
. . . . . . . . . . . . 13
|
31 | | elin 3796 |
. . . . . . . . . . . . . 14
|
32 | 31 | simplbi2 655 |
. . . . . . . . . . . . 13
|
33 | 9, 30, 32 | e33 38961 |
. . . . . . . . . . . 12
|
34 | | elin 3796 |
. . . . . . . . . . . . 13
|
35 | 34 | simplbi2com 657 |
. . . . . . . . . . . 12
|
36 | 6, 33, 35 | e33 38961 |
. . . . . . . . . . 11
|
37 | 36 | in3an 38836 |
. . . . . . . . . 10
|
38 | 37 | gen31 38846 |
. . . . . . . . 9
|
39 | | dfss2 3591 |
. . . . . . . . . 10
|
40 | 39 | biimpri 218 |
. . . . . . . . 9
|
41 | 38, 40 | e3 38964 |
. . . . . . . 8
|
42 | | idn3 38840 |
. . . . . . . . 9
|
43 | | simpr 477 |
. . . . . . . . 9
|
44 | 42, 43 | e3 38964 |
. . . . . . . 8
|
45 | | sseq0 3975 |
. . . . . . . . 9
|
46 | 45 | ex 450 |
. . . . . . . 8
|
47 | 41, 44, 46 | e33 38961 |
. . . . . . 7
|
48 | | simpl 473 |
. . . . . . . . 9
|
49 | 42, 48 | e3 38964 |
. . . . . . . 8
|
50 | | inss1 3833 |
. . . . . . . . 9
|
51 | 50 | sseli 3599 |
. . . . . . . 8
|
52 | 49, 51 | e3 38964 |
. . . . . . 7
|
53 | | pm3.21 464 |
. . . . . . 7
|
54 | 47, 52, 53 | e33 38961 |
. . . . . 6
|
55 | 54 | in3 38834 |
. . . . 5
|
56 | 55 | gen21 38844 |
. . . 4
|
57 | | exim 1761 |
. . . 4
|
58 | 56, 57 | e2 38856 |
. . 3
|
59 | | onfrALTlem3VD 39123 |
. . . 4
|
60 | | df-rex 2918 |
. . . . 5
|
61 | 60 | biimpi 206 |
. . . 4
|
62 | 59, 61 | e2 38856 |
. . 3
|
63 | | id 22 |
. . 3
|
64 | 58, 62, 63 | e22 38896 |
. 2
|
65 | | df-rex 2918 |
. . 3
|
66 | 65 | biimpri 218 |
. 2
|
67 | 64, 66 | e2 38856 |
1
|