NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  evenodddisjlem1 Unicode version

Theorem evenodddisjlem1 4515
Description: Lemma for evenodddisj 4516. Establish stratification for induction. (Contributed by SF, 25-Jan-2015.)
Assertion
Ref Expression
evenodddisjlem1 Nn 1c 1c
Distinct variable group:   ,

Proof of Theorem evenodddisjlem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-or 359 . . . 4 Nn 1c 1c Nn 1c 1c
2 vex 2862 . . . . . 6
32elimakv 4260 . . . . 5 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k
4 elin 3219 . . . . . . 7 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k
5 opkex 4113 . . . . . . . . . . . . 13
65elimak 4259 . . . . . . . . . . . 12 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
7 elpw121c 4148 . . . . . . . . . . . . . . . 16 1 1 1c
87anbi1i 676 . . . . . . . . . . . . . . 15 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
9 19.41v 1901 . . . . . . . . . . . . . . 15 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
108, 9bitr4i 243 . . . . . . . . . . . . . 14 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
1110exbii 1582 . . . . . . . . . . . . 13 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
12 df-rex 2620 . . . . . . . . . . . . 13 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
13 excom 1741 . . . . . . . . . . . . 13 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
1411, 12, 133bitr4i 268 . . . . . . . . . . . 12 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
15 snex 4111 . . . . . . . . . . . . . . 15
16 opkeq1 4059 . . . . . . . . . . . . . . . 16
1716eleq1d 2419 . . . . . . . . . . . . . . 15 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
1815, 17ceqsexv 2894 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
19 elsymdif 3223 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
20 snex 4111 . . . . . . . . . . . . . . . . . 18
21 vex 2862 . . . . . . . . . . . . . . . . . 18
2220, 21, 2otkelins3k 4256 . . . . . . . . . . . . . . . . 17 Ins3k Sk Sk
23 vex 2862 . . . . . . . . . . . . . . . . . 18
2423, 21elssetk 4270 . . . . . . . . . . . . . . . . 17 Sk
2522, 24bitri 240 . . . . . . . . . . . . . . . 16 Ins3k Sk
2620, 21, 2otkelins2k 4255 . . . . . . . . . . . . . . . . 17 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
27 opkex 4113 . . . . . . . . . . . . . . . . . . . 20
2827elimak 4259 . . . . . . . . . . . . . . . . . . 19 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
29 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . 23 1 1 1c
3029anbi1i 676 . . . . . . . . . . . . . . . . . . . . . 22 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
31 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
3230, 31bitr4i 243 . . . . . . . . . . . . . . . . . . . . 21 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
3332exbii 1582 . . . . . . . . . . . . . . . . . . . 20 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
34 df-rex 2620 . . . . . . . . . . . . . . . . . . . 20 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
35 excom 1741 . . . . . . . . . . . . . . . . . . . 20 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
3633, 34, 353bitr4i 268 . . . . . . . . . . . . . . . . . . 19 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
37 snex 4111 . . . . . . . . . . . . . . . . . . . . . 22
38 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . 23
3938eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
4037, 39ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
41 elin 3219 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
42 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24
4342, 20, 2otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Sk Sk
44 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24
4544, 2elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . 23 Sk
4643, 45bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Sk
47 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . 25
4847elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
49 elpw141c 4150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 1 1 1 1c
5049anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
51 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
5250, 51bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
5352exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
54 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
55 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
5653, 54, 553bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . 24 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
57 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
58 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5958eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
6057, 59ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
61 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
62 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6362, 37, 27otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k Ins2k Sk Ins2k Sk
64 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6564, 20, 2otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k Sk Sk
66 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6766, 2elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Sk
6863, 65, 673bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k Ins2k Sk
69 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
7062, 37, 27otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
71 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
72 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7371, 72opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
7464, 42opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk Ins3k Sk Ins2k Sk k1 1 1c
7566, 44opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 SIk Ins3k Sk Ins2k Sk k1 1 1c Ins3k Sk Ins2k Sk k1 1 1c
7666, 44ndisjrelk 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins3k Sk Ins2k Sk k1 1 1c
7776notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins3k Sk Ins2k Sk k1 1 1c
78 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7978elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins3k Sk Ins2k Sk k1 1 1c Ins3k Sk Ins2k Sk k1 1 1c
80 df-ne 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8180con2bii 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8277, 79, 813bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3k Sk Ins2k Sk k1 1 1c
8374, 75, 823bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
8470, 73, 833bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
85 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8685elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
87 elpw171c 4153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1 1 1 1 1 1 1 1c
8887anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
89 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
9088, 89bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
9190exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
92 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
93 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
9491, 92, 933bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
95 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
96 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9796eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
9895, 97ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
99 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
100 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
101100, 57, 47otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk Sk
102 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
103102, 37, 27otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Ins3k SIk Sk Ins3k SIk Sk
104 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
105104, 20, 2otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins3k SIk Sk SIk Sk
106 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
107106, 23opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 SIk Sk Sk
10821, 23elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Sk
109105, 107, 1083bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins3k SIk Sk
110101, 103, 1093bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2k Ins2k Ins3k SIk Sk
111100, 57, 47otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins3k SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk SIk Sk
112 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
113 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
114112, 113opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk Sk
115102, 62opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk SIk SIk Sk SIk SIk SIk Sk
116 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
117116, 71opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk SIk Sk SIk SIk Sk
118104, 64opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 SIk SIk Sk SIk Sk
119106, 66opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 SIk Sk Sk
12021, 66elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Sk
121118, 119, 1203bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk Sk
122115, 117, 1213bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SIk SIk SIk SIk Sk
123111, 114, 1223bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins3k SIk SIk SIk SIk SIk Sk
124100, 57, 47otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk Sk
125102, 37, 27otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins3k SIk SIk SIk Sk SIk SIk SIk Sk
126116, 72opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk SIk Sk SIk SIk Sk
127104, 42opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk Sk SIk Sk
128106, 44opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 SIk Sk Sk
12921, 44elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Sk
130128, 129bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk Sk
131126, 127, 1303bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SIk SIk SIk Sk
132124, 125, 1313bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins2k Ins3k SIk SIk SIk Sk
133123, 132orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
134 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
135 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
136133, 134, 1353bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
137110, 136bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
138137notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
13998, 99, 1383bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
140139exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
14186, 94, 1403bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
142141notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
14385elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
144 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
145 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
146144, 145bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
147142, 143, 1463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
14884, 147anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
14969, 148bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
15068, 149anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
15160, 61, 1503bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
152151exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
15348, 56, 1523bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
154 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . 23
155153, 154bitr4i 243 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
15646, 155anbi12i 678 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
15740, 41, 1563bitri 262 . . . . . . . . . . . . . . . . . . . 20 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
158157exbii 1582 . . . . . . . . . . . . . . . . . . 19 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
15928, 36, 1583bitri 262 . . . . . . . . . . . . . . . . . 18 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
160 df-rex 2620 . . . . . . . . . . . . . . . . . 18
161159, 160bitr4i 243 . . . . . . . . . . . . . . . . 17 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
162 rexcom 2772 . . . . . . . . . . . . . . . . 17
16326, 161, 1623bitri 262 . . . . . . . . . . . . . . . 16 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
16425, 163bibi12i 306 . . . . . . . . . . . . . . 15 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
165164notbii 287 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
16618, 19, 1653bitri 262 . . . . . . . . . . . . 13 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
167166exbii 1582 . . . . . . . . . . . 12 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
1686, 14, 1673bitri 262 . . . . . . . . . . 11 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
169168notbii 287 . . . . . . . . . 10 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
1705elcompl 3225 . . . . . . . . . 10 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
171 alex 1572 . . . . . . . . . 10
172169, 170, 1713bitr4i 268 . . . . . . . . 9 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
173 df-addc 4378 . . . . . . . . . . 11
174173eqeq2i 2363 . . . . . . . . . 10
175 abeq2 2458 . . . . . . . . . 10
176174, 175bitri 240 . . . . . . . . 9
177172, 176bitr4i 243 . . . . . . . 8 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
17821, 2opkelxpk 4248 . . . . . . . . . 10 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
1792, 178mpbiran2 885 . . . . . . . . 9 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
180 elun 3220 . . . . . . . . 9 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
18121elsnc 3756 . . . . . . . . . 10
18221elimak 4259 . . . . . . . . . . . . 13 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c
183 opkex 4113 . . . . . . . . . . . . . . . . 17
184183elimak 4259 . . . . . . . . . . . . . . . 16 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
185 elpw11c 4147 . . . . . . . . . . . . . . . . . . . 20 1 1c
186185anbi1i 676 . . . . . . . . . . . . . . . . . . 19 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
187 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
188186, 187bitr4i 243 . . . . . . . . . . . . . . . . . 18 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
189188exbii 1582 . . . . . . . . . . . . . . . . 17 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
190 df-rex 2620 . . . . . . . . . . . . . . . . 17 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
191 excom 1741 . . . . . . . . . . . . . . . . 17 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
192189, 190, 1913bitr4i 268 . . . . . . . . . . . . . . . 16 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
193 snex 4111 . . . . . . . . . . . . . . . . . . 19
194 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20
195194eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
196193, 195ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
197 elin 3219 . . . . . . . . . . . . . . . . . 18 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
198 vex 2862 . . . . . . . . . . . . . . . . . . . . 21
19923, 198, 21otkelins3k 4256 . . . . . . . . . . . . . . . . . . . 20 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c
200 opkex 4113 . . . . . . . . . . . . . . . . . . . . . 22
201200elimak 4259 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
202 elpw11c 4147 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1c
203202anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . 24 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
204 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
205203, 204bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . 23 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
206205exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
207 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . 22 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
208 excom 1741 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
209206, 207, 2083bitr4i 268 . . . . . . . . . . . . . . . . . . . . 21 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
210 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . 25
211210eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
212104, 211ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
213 elin 3219 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
214 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
215214elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
2167anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
217 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
218216, 217bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
219218exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
220 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
221 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
222219, 220, 2213bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
223 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
224223eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
22515, 224ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
226 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
22720, 21, 198otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins3k Sk Sk
228227, 24bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins3k Sk
229 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
230229elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
231 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 1 1 1c
232231anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
233 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
234232, 233bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
235234exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
236 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
237 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
238235, 236, 2373bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
239 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
240239eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
24162, 240ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
242 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
24364, 20, 198otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins2k Sk Sk
24466, 198elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Sk
245243, 244bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Sk
246 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
247246elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
248 elpw141c 4150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 1 1 1 1 1c
249248anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
250 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
251249, 250bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
252251exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
253 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
254 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
255252, 253, 2543bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
256 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
257 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
258257eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
259256, 258ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
260 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
26137, 62, 229otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins2k Ins2k Sk Ins2k Sk
26242, 20, 198otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins2k Sk Sk
26344, 198elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Sk
264261, 262, 2633bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins2k Ins2k Sk
265 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
26637, 62, 229otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
26737, 62opkelcnvk 4250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
26871, 72opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
26964, 42opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk Ins3k Sk Ins2k Sk k1 1 1c
27066, 44opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 SIk Ins3k Sk Ins2k Sk k1 1 1c Ins3k Sk Ins2k Sk k1 1 1c
271270, 76bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SIk Ins3k Sk Ins2k Sk k1 1 1c
272268, 269, 2713bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
273266, 267, 2723bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
274273notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
275 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
276275elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
277274, 276, 813bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
278275elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
27987anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
280 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
281279, 280bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
282281exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
283 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
284 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
285282, 283, 2843bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
286 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
287286eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
28895, 287ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
289 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
290100, 256, 246otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk Sk
291102, 62, 229otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins2k Ins3k SIk Sk Ins3k SIk Sk
292104, 20, 198otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Ins3k SIk Sk SIk Sk
293292, 107, 1083bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins3k SIk Sk
294290, 291, 2933bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Ins2k Ins2k Ins3k SIk Sk
295100, 256, 246otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk Sk
296102, 62, 229otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Ins3k SIk SIk SIk Sk SIk SIk SIk Sk
297119, 120bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 SIk Sk
298117, 118, 2973bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 SIk SIk SIk Sk
299295, 296, 2983bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Ins2k Ins3k SIk SIk SIk Sk
300100, 256, 246otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Ins3k SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk SIk Sk
301 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
302112, 301opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk Sk
303102, 37opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 SIk SIk SIk SIk Sk SIk SIk SIk Sk
304127, 128, 1293bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 SIk SIk Sk
305303, 126, 3043bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 SIk SIk SIk SIk Sk
306300, 302, 3053bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Ins3k SIk SIk SIk SIk SIk Sk
307299, 306orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
308 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
309307, 308, 1353bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
310294, 309bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
311310notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
312288, 289, 3113bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
313312exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
314278, 285, 3133bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
315314notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
316275elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
317315, 316, 1463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
318277, 317anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
319265, 318bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
320264, 319anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
321259, 260, 3203bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
322321exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
323247, 255, 3223bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
324 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
325323, 324bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
326245, 325anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
327241, 242, 3263bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
328327exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
329230, 238, 3283bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
33020, 21, 198otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
331 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
332329, 330, 3313bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
333228, 332bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
334333notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
335225, 226, 3343bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
336335exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
337215, 222, 3363bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
338337notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
339214elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
340 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . 26
341338, 339, 3403bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
34221, 23, 198otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
343 df-addc 4378 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
344343eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . . 26
345 abeq2 2458 . . . . . . . . . . . . . . . . . . . . . . . . . 26
346344, 345bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25
347341, 342, 3463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
34821, 23opkelimagek 4272 . . . . . . . . . . . . . . . . . . . . . . . . 25 Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck
34921, 23, 198otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
350 dfaddc2 4381 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1c Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck
351350eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . 25 1c Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck
352348, 349, 3513bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1c
353347, 352anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1c
354212, 213, 3533bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1c
355354exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1c
356201, 209, 3553bitri 262 . . . . . . . . . . . . . . . . . . . 20 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c 1c
357198, 198addcex 4394 . . . . . . . . . . . . . . . . . . . . 21
358 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . 22 1c 1c
359358eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 1c 1c
360357, 359ceqsexv 2894 . . . . . . . . . . . . . . . . . . . 20 1c 1c
361199, 356, 3603bitri 262 . . . . . . . . . . . . . . . . . . 19 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c 1c
36223, 198, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . 20 Ins2k k k k k
363 eldif 3221 . . . . . . . . . . . . . . . . . . . 20 k k k k
364 opkelidkg 4274 . . . . . . . . . . . . . . . . . . . . . . 23 k
36523, 21, 364mp2an 653 . . . . . . . . . . . . . . . . . . . . . 22 k
366 equcom 1680 . . . . . . . . . . . . . . . . . . . . . 22
367365, 366bitri 240 . . . . . . . . . . . . . . . . . . . . 21 k
36823, 21opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . . . . 24 k
36921, 368mpbiran2 885 . . . . . . . . . . . . . . . . . . . . . . 23 k
37023elsnc 3756 . . . . . . . . . . . . . . . . . . . . . . 23
371369, 370bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 k
372371notbii 287 . . . . . . . . . . . . . . . . . . . . 21 k
373367, 372anbi12i 678 . . . . . . . . . . . . . . . . . . . 20 k k
374362, 363, 3733bitri 262 . . . . . . . . . . . . . . . . . . 19 Ins2k k k
375361, 374anbi12i 678 . . . . . . . . . . . . . . . . . 18 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k 1c
376196, 197, 3753bitri 262 . . . . . . . . . . . . . . . . 17 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k 1c
377376exbii 1582 . . . . . . . . . . . . . . . 16 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k 1c
378184, 192, 3773bitri 262 . . . . . . . . . . . . . . 15 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c 1c
379 1cex 4142 . . . . . . . . . . . . . . . . 17 1c
380357, 379addcex 4394 . . . . . . . . . . . . . . . 16 1c
381 eqeq2 2362 . . . . . . . . . . . . . . . . 17 1c 1c
382 eqeq1 2359 . . . . . . . . . . . . . . . . . 18 1c 1c
383382notbid 285 . . . . . . . . . . . . . . . . 17 1c 1c
384381, 383anbi12d 691 . . . . . . . . . . . . . . . 16 1c 1c 1c
385380, 384ceqsexv 2894 . . . . . . . . . . . . . . 15 1c 1c 1c
386 annim 414 . . . . . . . . . . . . . . 15 1c 1c 1c 1c
387378, 385, 3863bitri 262 . . . . . . . . . . . . . 14 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c 1c 1c
388387rexbii 2639 . . . . . . . . . . . . 13 Nn Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c Nn 1c 1c
389182, 388bitri 240 . . . . . . . . . . . 12 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn 1c 1c
390389notbii 287 . . . . . . . . . . 11 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn 1c 1c
39121elcompl 3225 . . . . . . . . . . 11 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
392 df-ne 2518 . . . . . . . . . . . . . . 15 1c 1c
393 df-ne 2518 . . . . . . . . . . . . . . 15 1c 1c
394392, 393imbi12i 316 . . . . . . . . . . . . . 14 1c 1c 1c 1c
395 con34b 283 . . . . . . . . . . . . . 14 1c 1c 1c 1c
396394, 395bitr4i 243 . . . . . . . . . . . . 13 1c 1c 1c 1c
397396ralbii 2638 . . . . . . . . . . . 12 Nn 1c 1c Nn 1c 1c
398 dfral2 2626 . . . . . . . . . . . 12 Nn 1c 1c Nn 1c 1c
399397, 398bitri 240 . . . . . . . . . . 11 Nn 1c 1c Nn 1c 1c
400390, 391, 3993bitr4i 268 . . . . . . . . . 10 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn 1c 1c
401181, 400orbi12i 507 . . . . . . . . 9 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn 1c 1c
402179, 180, 4013bitri 262 . . . . . . . 8 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Nn 1c 1c
403177, 402anbi12i 678 . . . . . . 7 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Nn 1c 1c
4044, 403bitri 240 . . . . . 6 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Nn 1c 1c
405404exbii 1582 . . . . 5 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Nn 1c 1c
4062, 2addcex 4394 . . . . . 6
407 eqeq1 2359 . . . . . . 7
408 neeq1 2524 . . . . . . . . 9 1c 1c
409408imbi2d 307 . . . . . . . 8 1c 1c 1c 1c
410409ralbidv 2634 . . . . . . 7 Nn 1c 1c Nn 1c 1c
411407, 410orbi12d 690 . . . . . 6 Nn 1c 1c Nn 1c 1c
412406, 411ceqsexv 2894 . . . . 5 Nn 1c 1c Nn 1c 1c
4133, 405, 4123bitri 262 . . . 4 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k Nn 1c 1c
414 df-ne 2518 . . . . 5
415414imbi1i 315 . . . 4 Nn 1c 1c Nn 1c 1c
4161, 413, 4153bitr4i 268 . . 3 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k Nn 1c 1c
417416abbi2i 2464 . 2 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k Nn 1c 1c
418 ssetkex 4294 . . . . . . . 8 Sk
419418ins3kex 4308 . . . . . . 7 Ins3k Sk
420418ins2kex 4307 . . . . . . . . . 10 Ins2k Sk
421420ins2kex 4307 . . . . . . . . . . . 12 Ins2k Ins2k Sk
422419, 420inex 4105 . . . . . . . . . . . . . . . . . . 19 Ins3k Sk Ins2k Sk
423379pw1ex 4303 . . . . . . . . . . . . . . . . . . . 20 1 1c
424423pw1ex 4303 . . . . . . . . . . . . . . . . . . 19 1 1 1c
425422, 424imakex 4300 . . . . . . . . . . . . . . . . . 18 Ins3k Sk Ins2k Sk k1 1 1c
426425complex 4104 . . . . . . . . . . . . . . . . 17 Ins3k Sk Ins2k Sk k1 1 1c
427426sikex 4297 . . . . . . . . . . . . . . . 16 SIk Ins3k Sk Ins2k Sk k1 1 1c
428427sikex 4297 . . . . . . . . . . . . . . 15 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
429428sikex 4297 . . . . . . . . . . . . . 14 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
430429ins3kex 4308 . . . . . . . . . . . . 13 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
431418sikex 4297 . . . . . . . . . . . . . . . . . . 19 SIk Sk
432431ins3kex 4308 . . . . . . . . . . . . . . . . . 18 Ins3k SIk Sk
433432ins2kex 4307 . . . . . . . . . . . . . . . . 17 Ins2k Ins3k SIk Sk
434433ins2kex 4307 . . . . . . . . . . . . . . . 16 Ins2k Ins2k Ins3k SIk Sk
435431sikex 4297 . . . . . . . . . . . . . . . . . . . . 21 SIk SIk Sk
436435sikex 4297 . . . . . . . . . . . . . . . . . . . 20 SIk SIk SIk Sk
437436sikex 4297 . . . . . . . . . . . . . . . . . . 19 SIk SIk SIk SIk Sk
438437sikex 4297 . . . . . . . . . . . . . . . . . 18 SIk SIk SIk SIk SIk Sk
439438ins3kex 4308 . . . . . . . . . . . . . . . . 17 Ins3k SIk SIk SIk SIk SIk Sk
440436ins3kex 4308 . . . . . . . . . . . . . . . . . 18 Ins3k SIk SIk SIk Sk
441440ins2kex 4307 . . . . . . . . . . . . . . . . 17 Ins2k Ins3k SIk SIk SIk Sk
442439, 441unex 4106 . . . . . . . . . . . . . . . 16 Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
443434, 442symdifex 4108 . . . . . . . . . . . . . . 15 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
444424pw1ex 4303 . . . . . . . . . . . . . . . . . . 19 1 1 1 1c
445444pw1ex 4303 . . . . . . . . . . . . . . . . . 18 1 1 1 1 1c
446445pw1ex 4303 . . . . . . . . . . . . . . . . 17 1 1 1 1 1 1c
447446pw1ex 4303 . . . . . . . . . . . . . . . 16 1 1 1 1 1 1 1c
448447pw1ex 4303 . . . . . . . . . . . . . . 15 1 1 1 1 1 1 1 1c
449443, 448imakex 4300 . . . . . . . . . . . . . 14 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
450449complex 4104 . . . . . . . . . . . . 13 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
451430, 450inex 4105 . . . . . . . . . . . 12 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
452421, 451inex 4105 . . . . . . . . . . 11 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
453452, 445imakex 4300 . . . . . . . . . 10 Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
454420, 453inex 4105 . . . . . . . . 9 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
455454, 424imakex 4300 . . . . . . . 8 Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
456455ins2kex 4307 . . . . . . 7 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
457419, 456symdifex 4108 . . . . . 6 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
458457, 424imakex 4300 . . . . 5 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
459458complex 4104 . . . 4 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
460 snex 4111 . . . . . 6
461425sikex 4297 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SIk Ins3k Sk Ins2k Sk k1 1 1c
462461sikex 4297 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
463462sikex 4297 . . . . . . . . . . . . . . . . . . . . . . . . . 26 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
464463cnvkex 4287 . . . . . . . . . . . . . . . . . . . . . . . . 25 k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
465464ins3kex 4308 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
466465complex 4104 . . . . . . . . . . . . . . . . . . . . . . 23 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
467441, 439unex 4106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
468434, 467symdifex 4108 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
469468, 448imakex 4300 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
470469complex 4104 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
471466, 470inex 4105 . . . . . . . . . . . . . . . . . . . . . 22 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
472421, 471inex 4105 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
473472, 445imakex 4300 . . . . . . . . . . . . . . . . . . . 20 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
474420, 473inex 4105 . . . . . . . . . . . . . . . . . . 19 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
475474, 424imakex 4300 . . . . . . . . . . . . . . . . . 18 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
476475ins2kex 4307 . . . . . . . . . . . . . . . . 17 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
477419, 476symdifex 4108 . . . . . . . . . . . . . . . 16 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
478477, 424imakex 4300 . . . . . . . . . . . . . . 15 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
479478complex 4104 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
480479ins2kex 4307 . . . . . . . . . . . . 13 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
481 addcexlem 4382 . . . . . . . . . . . . . . . 16 Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1c
482481, 424imakex 4300 . . . . . . . . . . . . . . 15 Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
483482imagekex 4312 . . . . . . . . . . . . . 14 Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
484483ins3kex 4308 . . . . . . . . . . . . 13 Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
485480, 484inex 4105 . . . . . . . . . . . 12 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
486485, 423imakex 4300 . . . . . . . . . . 11 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c
487486ins3kex 4308 . . . . . . . . . 10 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c
488 idkex 4314 . . . . . . . . . . . 12 k
489 vvex 4109 . . . . . . . . . . . . 13
490460, 489xpkex 4289 . . . . . . . . . . . 12 k
491488, 490difex 4107 . . . . . . . . . . 11 k k
492491ins2kex 4307 . . . . . . . . . 10 Ins2k k k
493487, 492inex 4105 . . . . . . . . 9 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
494493, 423imakex 4300 . . . . . . . 8 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c
495 nncex 4396 . . . . . . . 8 Nn
496494, 495imakex 4300 . . . . . . 7 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
497496complex 4104 . . . . . 6 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
498460, 497unex 4106 . . . . 5 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
499498, 489xpkex 4289 . . . 4 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k
500459, 499inex 4105 . . 3 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k
501500, 489imakex 4300 . 2 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k
502417, 501eqeltrri 2424 1 Nn 1c 1c
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358  wal 1540  wex 1541   wceq 1642   wcel 1710  cab 2339   wne 2516  wral 2614  wrex 2615  cvv 2859   ∼ ccompl 3205   cdif 3206   cun 3207   cin 3208   csymdif 3209  c0 3550  csn 3737  copk 4057  1cc1c 4134  1 cpw1 4135   k cxpk 4174  kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177  kcimak 4179   SIk csik 4181  Imagekcimagek 4182   Sk cssetk 4183   k cidk 4184   Nn cnnc 4373   cplc 4375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-addc 4378  df-nnc 4379
This theorem is referenced by:  evenodddisj  4516
  Copyright terms: Public domain W3C validator