Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . 5
|
2 | 1 | eluni1 4173 |
. . . 4
⋃1 ∼
SIk Sk SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1c ∼ SIk Sk SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1c |
3 | | snex 4111 |
. . . . . . . . . 10
|
4 | | opkeq1 4059 |
. . . . . . . . . . 11
|
5 | 4 | eleq1d 2419 |
. . . . . . . . . 10
SIk Sk SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1c
SIk Sk SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1c |
6 | 3, 5 | ceqsexv 2894 |
. . . . . . . . 9
SIk Sk SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1c
SIk Sk SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1c |
7 | | elin 3219 |
. . . . . . . . 9
SIk Sk SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1c SIk Sk
SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1c |
8 | | snex 4111 |
. . . . . . . . . . . 12
|
9 | 8, 1 | opksnelsik 4265 |
. . . . . . . . . . 11
SIk Sk Sk |
10 | | vex 2862 |
. . . . . . . . . . . 12
|
11 | 10, 1 | elssetk 4270 |
. . . . . . . . . . 11
Sk |
12 | 9, 11 | bitri 240 |
. . . . . . . . . 10
SIk Sk |
13 | | eldif 3221 |
. . . . . . . . . . 11
SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1c
SIk 1 Nn k Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1ck1 1c |
14 | 8, 1 | opksnelsik 4265 |
. . . . . . . . . . . . 13
SIk 1 Nn k
1 Nn k |
15 | 8, 1 | opkelxpk 4248 |
. . . . . . . . . . . . . . 15
1 Nn k
1 Nn |
16 | 1, 15 | mpbiran2 885 |
. . . . . . . . . . . . . 14
1 Nn k
1 Nn |
17 | | snelpw1 4146 |
. . . . . . . . . . . . . 14
1 Nn Nn |
18 | 16, 17 | bitri 240 |
. . . . . . . . . . . . 13
1 Nn k
Nn |
19 | 10 | elpw 3728 |
. . . . . . . . . . . . 13
Nn
Nn |
20 | 14, 18, 19 | 3bitri 262 |
. . . . . . . . . . . 12
SIk 1 Nn k Nn |
21 | | snex 4111 |
. . . . . . . . . . . . . . . . 17
|
22 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . 18
|
23 | 22 | eleq1d 2419 |
. . . . . . . . . . . . . . . . 17
Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1c
Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1c |
24 | 21, 23 | ceqsexv 2894 |
. . . . . . . . . . . . . . . 16
Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1c
Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1c |
25 | | elin 3219 |
. . . . . . . . . . . . . . . 16
Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1c
Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k
Ins3k Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1c |
26 | | vex 2862 |
. . . . . . . . . . . . . . . . . . 19
|
27 | | snex 4111 |
. . . . . . . . . . . . . . . . . . 19
|
28 | 26, 3, 27 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . 18
Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
29 | 26, 27 | opkelcnvk 4250 |
. . . . . . . . . . . . . . . . . 18
k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k
k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
30 | 1, 26 | eqtfinrelk 4486 |
. . . . . . . . . . . . . . . . . 18
k
∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Tfin
|
31 | 28, 29, 30 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
Ins2k k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Tfin
|
32 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 32 | elimak 4259 |
. . . . . . . . . . . . . . . . . . 19
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk k1 1 1c 1 1 1c Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
34 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . . . . 23
1 1 1c |
35 | 34 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . 22
1 1
1c
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
36 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . 22
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
37 | 35, 36 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . 21
1 1
1c
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
38 | 37 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . 20
1 1 1c
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
39 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . 20
1 1
1c
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk 1 1 1c Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
40 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . 20
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
41 | 38, 39, 40 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . 19
1 1
1c
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
42 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . 22
|
43 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
44 | 43 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . 22
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
45 | 42, 44 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . 21
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
46 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . 21
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c Ins3k Sk |
47 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
48 | 47, 26, 3 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . 23
Ins2k SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c |
49 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
50 | 49, 8 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . 23
SIk ∼ Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c ∼
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c |
51 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
52 | 51 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1ck1 1 1c 1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
53 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
1 1 1c |
54 | 53 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1 1
1c Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
55 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
56 | 54, 55 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1 1
1c Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
57 | 56 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
58 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1 1
1c Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c 1 1
1c Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
59 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
60 | 57, 58, 59 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
1 1
1c Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
61 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
62 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
63 | 62 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
64 | 61, 63 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
65 | | elsymdif 3223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c Ins3k Sk Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
66 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
67 | 66, 49, 8 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins3k Sk Sk |
68 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
69 | 68, 49 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Sk |
70 | 67, 69 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins3k Sk |
71 | 66, 49, 8 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins2k SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c SIk Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c |
72 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
73 | 72 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k k1 1 1c 1 1 1c
Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
74 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
1 1 1c |
75 | 74 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
1 1
1c Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k
Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
76 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k
Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
77 | 75, 76 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
1 1
1c Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
78 | 77 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
1 1 1c Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
79 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
1 1
1c Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k 1 1 1c
Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
80 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k |
81 | 78, 79, 80 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
1 1
1c Ins2k Sk Ins3k k ∼ Ins2k Sk Ins3k Ins3k k
Sk Ins2k Ins2k Nn k Ins2k SIk Sk Ins3k Ins3k SIk 1c k
Ins3k Sk Ins2k SIk Sk k1 1 1 1c
Ins2k Sk k1 1 1ck1 1 1 1c
Ins3k k k1 1ck1 1ck1 1 1c k
Ins2k Sk Ins3k |