Step | Hyp | Ref
| Expression |
1 | | snex 4111 |
. . . . . . . . . 10
![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) |
2 | 1 | snid 3760 |
. . . . . . . . 9
![{](lbrace.gif) ![(/)](varnothing.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![}](rbrace.gif) |
3 | | eqtfinrelk.2 |
. . . . . . . . . 10
![_V](rmcv.gif) |
4 | 1, 3 | opkelxpk 4248 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 2, 4 | mpbiran 884 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
6 | 3 | elsnc 3756 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
7 | 5, 6 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
8 | 7 | orbi1i 506 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | elun 3220 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 1, 3 | opkelxpk 4248 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 2, 3, 10 | mpbir2an 886 |
. . . . . . . . . 10
![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) |
12 | 11 | notnoti 115 |
. . . . . . . . 9
![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) |
13 | 12 | intnan 880 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | eldif 3221 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 13, 14 | mtbir 290 |
. . . . . . 7
![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | biorfi 396 |
. . . . . 6
![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 8, 9, 16 | 3bitr4i 268 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
18 | 17 | a1i 10 |
. . . 4
![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | sneq 3744 |
. . . . . 6
![(](lp.gif)
![{](lbrace.gif) ![M](_cm.gif)
![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
20 | 19 | opkeq1d 4065 |
. . . . 5
![(](lp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) ![)](rp.gif) |
21 | 20 | eleq1d 2419 |
. . . 4
![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | | iftrue 3668 |
. . . . 5
![(](lp.gif)
![if](_if.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
23 | 22 | eqeq2d 2364 |
. . . 4
![(](lp.gif)
![(](lp.gif)
![if](_if.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 18, 21, 23 | 3bitr4d 276 |
. . 3
![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![if](_if.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | iffalse 3669 |
. . . . 5
![(](lp.gif) ![if](_if.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | eqeq2d 2364 |
. . . 4
![(](lp.gif) ![(](lp.gif)
![if](_if.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | opkex 4113 |
. . . . . . . . 9
![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![_V](rmcv.gif) |
28 | 27 | elimak 4259 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![E.](exists.gif) 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | elpw121c 4148 |
. . . . . . . . . . . 12
![(](lp.gif) 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
30 | 29 | anbi1i 676 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | 19.41v 1901 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 30, 31 | bitr4i 243 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 32 | exbii 1582 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | df-rex 2620 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | | excom 1741 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 33, 34, 35 | 3bitr4i 268 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif)
![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | snex 4111 |
. . . . . . . . . . 11
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
38 | | opkeq1 4059 |
. . . . . . . . . . . 12
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
39 | 38 | eleq1d 2419 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 37, 39 | ceqsexv 2894 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | elsymdif 3223 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | | snex 4111 |
. . . . . . . . . . . . . 14
![{](lbrace.gif) ![z](_z.gif)
![_V](rmcv.gif) |
43 | | snex 4111 |
. . . . . . . . . . . . . 14
![{](lbrace.gif) ![M](_cm.gif)
![_V](rmcv.gif) |
44 | 42, 43, 3 | otkelins2k 4255 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![X](_cx.gif) Sk ![)](rp.gif) |
45 | | vex 2862 |
. . . . . . . . . . . . . 14
![_V](rmcv.gif) |
46 | 45, 3 | elssetk 4270 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![X](_cx.gif) Sk ![X](_cx.gif) ![)](rp.gif) |
47 | 44, 46 | bitri 240 |
. . . . . . . . . . . 12
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk ![X](_cx.gif) ![)](rp.gif) |
48 | | snex 4111 |
. . . . . . . . . . . . . . . 16
![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
49 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
50 | 49 | eleq1d 2419 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 48, 50 | ceqsexv 2894 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | | eldif 3221 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
![_V](rmcv.gif) |
54 | 53, 42, 43 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k k
Sk ![<<](llangle.gif) ![n](_n.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) k
Sk ![)](rp.gif) |
55 | 53, 42 | opkelcnvk 4250 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) k Sk
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![n](_n.gif) Sk ![)](rp.gif) |
56 | 45, 53 | elssetk 4270 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![n](_n.gif) Sk ![n](_n.gif) ![)](rp.gif) |
57 | 54, 55, 56 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k k
Sk ![n](_n.gif) ![)](rp.gif) |
58 | 53, 42, 43 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) |
59 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . 20
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
60 | 59 | elimak 4259 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c ![E.](exists.gif) 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) |
61 | | elpw11c 4147 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
62 | 61 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
63 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 62, 63 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 64 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
66 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif)
1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
67 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
68 | 65, 66, 67 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![E.](exists.gif)
1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
69 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . 22
![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
70 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
71 | 70 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
72 | 69, 71 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![)](rp.gif) |
73 | | elsymdif 3223 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k k
![)](rp.gif) ![)](rp.gif) |
74 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![_V](rmcv.gif) |
75 | 74, 53, 43 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
76 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Nn k ![_V](rmcv.gif)
![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) Nn k ![_V](rmcv.gif)
![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
77 | 74, 43 | opkelxpk 4248 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) Nn k ![_V](rmcv.gif)
![(](lp.gif) Nn ![{](lbrace.gif) ![M](_cm.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
78 | 43, 77 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) Nn k ![_V](rmcv.gif)
Nn ![)](rp.gif) |
79 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
80 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
81 | 80 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
82 | 79, 81 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
83 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
84 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
85 | 84, 74, 43 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) SIk Sk ![)](rp.gif) |
86 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![{](lbrace.gif) ![a](_a.gif)
![_V](rmcv.gif) |
87 | | eqtfinrelk.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![_V](rmcv.gif) |
88 | 86, 87 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![M](_cm.gif) Sk ![)](rp.gif) |
89 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![_V](rmcv.gif) |
90 | 89, 87 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![M](_cm.gif) Sk ![M](_cm.gif) ![)](rp.gif) |
91 | 85, 88, 90 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk ![M](_cm.gif) ![)](rp.gif) |
92 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![_V](rmcv.gif) |
93 | 92 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif)
![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c ![E.](exists.gif) 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) |
94 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
95 | 94 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
96 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
97 | 95, 96 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 97 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
99 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
100 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
101 | 98, 99, 100 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
102 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
103 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![y](_y.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
104 | 103 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
105 | 102, 104 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) ![)](rp.gif) |
106 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![y](_y.gif) ![>>](rrangle.gif) Ins3k
SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins2k
Sk ![)](rp.gif) ![)](rp.gif) |
107 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
108 | 107, 84, 74 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif)
SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
109 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![_V](rmcv.gif) |
110 | 109, 86 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![x](_x.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
111 | 109, 89 | eqpw1relk 4479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![x](_x.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif) ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
1 ![a](_a.gif) ![)](rp.gif) |
112 | 108, 110,
111 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
1 ![a](_a.gif) ![)](rp.gif) |
113 | 107, 84, 74 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![y](_y.gif) Sk ![)](rp.gif) |
114 | 109, 74 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![y](_y.gif) Sk ![y](_y.gif) ![)](rp.gif) |
115 | 113, 114 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins2k Sk ![y](_y.gif) ![)](rp.gif) |
116 | 112, 115 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins2k
Sk ![(](lp.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
117 | 105, 106,
116 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif)
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![(](lp.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
118 | 117 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif) ![>>](rrangle.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
119 | 93, 101, 118 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![y](_y.gif)
![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
120 | 84, 74, 43 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![y](_y.gif) ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
121 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) 1
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
122 | 119, 120,
121 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c 1
![y](_y.gif) ![)](rp.gif) |
123 | 91, 122 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![(](lp.gif) 1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
124 | 82, 83, 123 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) 1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
125 | 124 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif)
1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
126 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![E.](exists.gif)
1 1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
127 | | elpw131c 4149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) 1 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
128 | 127 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
129 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
130 | 128, 129 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
131 | 130 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
132 | 126, 131 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![E.](exists.gif)
1 1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
133 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
134 | 133 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c ![E.](exists.gif) 1 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
135 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
136 | 132, 134,
135 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c ![E.](exists.gif) ![a](_a.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
137 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![E.](exists.gif)
1 ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif)
1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
138 | 125, 136,
137 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c ![E.](exists.gif) 1 ![y](_y.gif) ![)](rp.gif) |
139 | 78, 138 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) Nn k ![_V](rmcv.gif)
![<<](llangle.gif) ![y](_y.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![(](lp.gif) Nn ![E.](exists.gif) 1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
140 | 75, 76, 139 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![(](lp.gif) Nn ![E.](exists.gif) 1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
141 | 74, 53, 43 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k ![<<](llangle.gif) ![y](_y.gif) ![n](_n.gif)
k ![)](rp.gif) |
142 | | opkelidkg 4274 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif)
![_V](rmcv.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![n](_n.gif) k ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
143 | 74, 53, 142 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![n](_n.gif) k ![n](_n.gif) ![)](rp.gif) |
144 | 141, 143 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k ![n](_n.gif) ![)](rp.gif) |
145 | 140, 144 | bibi12i 306 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k k
![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
146 | 73, 145 | xchbinx 301 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
147 | 72, 146 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
148 | 147 | exbii 1582 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
149 | 60, 68, 148 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
150 | | exnal 1574 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![n](_n.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
151 | 58, 149, 150 | 3bitrri 263 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![n](_n.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) |
152 | 151 | con1bii 321 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
153 | 57, 152 | anbi12i 678 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
154 | 51, 52, 153 | 3bitri 262 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
155 | 154 | exbii 1582 |
. . . . . . . . . . . . 13
![(](lp.gif) ![E.](exists.gif) ![n](_n.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif)
![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
156 | 42, 43, 3 | otkelins3k 4256 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) |
157 | | opkex 4113 |
. . . . . . . . . . . . . . 15
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
158 | 157 | elimak 4259 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c ![E.](exists.gif) 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
159 | | elpw11c 4147 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
160 | 159 | anbi1i 676 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
161 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
162 | 160, 161 | bitr4i 243 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
163 | 162 | exbii 1582 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
164 | | df-rex 2620 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif)
1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
165 | | excom 1741 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif) ![n](_n.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
166 | 163, 164,
165 | 3bitr4i 268 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif)
1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![E.](exists.gif) ![n](_n.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
167 | 156, 158,
166 | 3bitri 262 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c ![E.](exists.gif) ![n](_n.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k k Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
168 | | dfiota2 4340 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![U.](bigcup.gif) ![{](lbrace.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![}](rbrace.gif) |
169 | 168 | eleq2i 2417 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif)
Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif)
![U.](bigcup.gif) ![{](lbrace.gif)
![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
170 | | eluniab 3903 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![U.](bigcup.gif) ![{](lbrace.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
171 | 169, 170 | bitri 240 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif)
Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif)
![E.](exists.gif) ![n](_n.gif) ![(](lp.gif)
![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
172 | 155, 167,
171 | 3bitr4i 268 |
. . . . . . . . . . . 12
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
173 | 47, 172 | bibi12i 306 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
174 | 41, 173 | xchbinx 301 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif)
![(](lp.gif)
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
175 | 40, 174 | bitri 240 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
176 | 175 | exbii 1582 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
177 | 28, 36, 176 | 3bitri 262 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
178 | 177 | notbii 287 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
179 | 27 | elcompl 3225 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif)
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
180 | | dfcleq 2347 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif)
Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif)
![A.](forall.gif) ![z](_z.gif) ![(](lp.gif)
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
181 | | alex 1572 |
. . . . . . 7
![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif)
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
182 | 180, 181 | bitri 240 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif)
Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif)
![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif) 1
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
183 | 178, 179,
182 | 3bitr4i 268 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
184 | 183 | a1i 10 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
185 | 43, 3 | opkelxpk 4248 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif)
![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
186 | 3 | biantru 491 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
187 | 43 | elsnc 3756 |
. . . . . . . . . . . 12
![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![M](_cm.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
188 | 87 | sneqb 3876 |
. . . . . . . . . . . 12
![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
189 | 187, 188 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
190 | 185, 186,
189 | 3bitr2i 264 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
191 | 190 | biimpi 186 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
192 | 191 | con3i 127 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
193 | 192 | biantrud 493 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
194 | | simpl 443 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
195 | 194 | con3i 127 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
196 | | biorf 394 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
197 | 195, 196 | syl 15 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
198 | 193, 197 | bitrd 244 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
199 | 43, 3 | opkelxpk 4248 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
200 | 189, 6 | anbi12i 678 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
201 | 199, 200 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
202 | | eldif 3221 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
203 | 201, 202 | orbi12i 507 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ∼ ![(](lp.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
204 | 198, 203 | syl6bbr 254 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif)
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![X](_cx.gif) ∼ ![(](lp.gif)
Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
205 | | elun 3220 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
206 | 204, 205 | syl6bbr 254 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ∼
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
207 | 26, 184, 206 | 3bitr2rd 273 |
. . 3
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![if](_if.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
208 | 24, 207 | pm2.61i 156 |
. 2
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![if](_if.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
209 | | df-tfin 4443 |
. . 3
Tfin
![if](_if.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
210 | 209 | eqeq2i 2363 |
. 2
![(](lp.gif) Tfin
![if](_if.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![iota](riota.gif) ![y](_y.gif) ![(](lp.gif) Nn ![E.](exists.gif)
1 ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
211 | 208, 210 | bitr4i 243 |
1
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) Tfin ![M](_cm.gif) ![)](rp.gif) |