Step | Hyp | Ref
| Expression |
1 | | snex 4111 |
. . . . 5
![{](lbrace.gif) ![B](_cb.gif)
![_V](rmcv.gif) |
2 | | eqpw1relk.1 |
. . . . . 6
![_V](rmcv.gif) |
3 | 2, 1 | opkelxpk 4248 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) 1c
k
![_V](rmcv.gif) ![(](lp.gif)
1c ![{](lbrace.gif) ![B](_cb.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 1, 3 | mpbiran2 885 |
. . . 4
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) 1c
k
![_V](rmcv.gif)
1c![)](rp.gif) |
5 | 2 | elpw 3728 |
. . . 4
![(](lp.gif) 1c
1c![)](rp.gif) |
6 | 4, 5 | bitri 240 |
. . 3
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) 1c
k
![_V](rmcv.gif) 1c![)](rp.gif) |
7 | | opkex 4113 |
. . . . . . 7
![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
8 | 7 | elimak 4259 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c ![E.](exists.gif) 1 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) |
9 | | elpw131c 4149 |
. . . . . . . . . 10
![(](lp.gif) 1 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
10 | 9 | anbi1i 676 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | 19.41v 1901 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 10, 11 | bitr4i 243 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | df-rex 2620 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
1 1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | | excom 1741 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 13, 14, 15 | 3bitr4i 268 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
1 1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 8, 16 | bitri 240 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | snex 4111 |
. . . . . . . 8
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
19 | | opkeq1 4059 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
20 | 19 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 18, 20 | ceqsexv 2894 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) |
22 | | elsymdif 3223 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk ![)](rp.gif) ![)](rp.gif) |
23 | | snex 4111 |
. . . . . . . . . . 11
![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
24 | 23, 2, 1 | otkelins3k 4256 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![A](_ca.gif)
Sk ![)](rp.gif) |
25 | | snex 4111 |
. . . . . . . . . . 11
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
26 | 25, 2 | elssetk 4270 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![A](_ca.gif)
Sk ![{](lbrace.gif) ![x](_x.gif) ![A](_ca.gif) ![)](rp.gif) |
27 | 24, 26 | bitri 240 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk ![{](lbrace.gif) ![x](_x.gif) ![A](_ca.gif) ![)](rp.gif) |
28 | 23, 2, 1 | otkelins2k 4255 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) SIk Sk ![)](rp.gif) |
29 | | eqpw1relk.2 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
30 | 25, 29 | opksnelsik 4265 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk ![)](rp.gif) |
31 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
32 | 31, 29 | elssetk 4270 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk ![B](_cb.gif) ![)](rp.gif) |
33 | 30, 32 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) SIk Sk ![B](_cb.gif) ![)](rp.gif) |
34 | 28, 33 | bitri 240 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk ![B](_cb.gif) ![)](rp.gif) |
35 | 27, 34 | bibi12i 306 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins2k SIk Sk ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 22, 35 | xchbinx 301 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 21, 36 | bitri 240 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k SIk Sk ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 37 | exbii 1582 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif)
![E.](exists.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | exnal 1574 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![B](_cb.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 17, 38, 39 | 3bitrri 263 |
. . . 4
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![B](_cb.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif) ![)](rp.gif) |
41 | 40 | con1bii 321 |
. . 3
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 6, 41 | anbi12i 678 |
. 2
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![(](lp.gif) 1c ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | | eldif 3221 |
. 2
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.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)
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif) ![(](lp.gif) 1c
k
![_V](rmcv.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.gif) ![}](rbrace.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | eqpw1 4162 |
. 2
![(](lp.gif) 1 ![(](lp.gif) 1c ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 42, 43, 44 | 3bitr4i 268 |
1
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![{](lbrace.gif) ![B](_cb.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 ![B](_cb.gif) ![)](rp.gif) |