Step | Hyp | Ref
| Expression |
1 | | iftrue 3668 |
. . . . . . . . 9
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
2 | 1 | eqeq2d 2364 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | iba 489 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | simpr 447 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
Nn Nn ![)](rp.gif) |
5 | 4 | con2i 112 |
. . . . . . . . . 10
![(](lp.gif) Nn ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) |
6 | | biorf 394 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c Nn ![(](lp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c
Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 5, 6 | syl 15 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | orcom 376 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c Nn ![(](lp.gif)
Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 7, 8 | syl6bb 252 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 2, 3, 9 | 3bitrd 270 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c Nn ![(](lp.gif)
Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | iffalse 3669 |
. . . . . . . . 9
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![y](_y.gif) ![)](rp.gif) |
12 | 11 | eqeq2d 2364 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | iba 489 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | simpr 447 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c Nn Nn ![)](rp.gif) |
15 | 14 | con3i 127 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c
Nn ![)](rp.gif) ![)](rp.gif) |
16 | | biorf 394 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 15, 16 | syl 15 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c
Nn ![(](lp.gif)
Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 12, 13, 17 | 3bitrd 270 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 10, 18 | pm2.61i 156 |
. . . . . 6
![(](lp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | equcom 1680 |
. . . . . . . 8
![(](lp.gif) ![y](_y.gif) ![)](rp.gif) |
21 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
22 | 21 | elcompl 3225 |
. . . . . . . 8
![(](lp.gif) ∼ Nn Nn ![)](rp.gif) |
23 | 20, 22 | anbi12i 678 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
∼ Nn ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) |
24 | 23 | orbi2i 505 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ∼ Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 19, 24 | bitr4i 243 |
. . . . 5
![(](lp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ∼ Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | elun 3220 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | elin 3219 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | | vex 2862 |
. . . . . . . . . . 11
![_V](rmcv.gif) |
29 | 21, 28 | opkelimagek 4272 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | dfaddc2 4381 |
. . . . . . . . . . 11
![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) Ins3k ∼
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k![y](_y.gif) ![)](rp.gif) |
31 | 30 | eqeq2i 2363 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) Ins3k ∼
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 29, 31 | bitr4i 243 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
33 | 21, 28 | opkelxpk 4248 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif)
Nn ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 28, 33 | mpbiran2 885 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Nn k ![_V](rmcv.gif)
Nn ![)](rp.gif) |
35 | 32, 34 | anbi12i 678 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Imagek![(](lp.gif) Ins3k ∼
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Nn k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1c
Nn ![)](rp.gif) ![)](rp.gif) |
36 | 27, 35 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1c
Nn ![)](rp.gif) ![)](rp.gif) |
37 | | elin 3219 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) k ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | | opkelidkg 4274 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
![_V](rmcv.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) k ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 21, 28, 38 | mp2an 653 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) k ![x](_x.gif) ![)](rp.gif) |
40 | 21, 28 | opkelxpk 4248 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ∼ Nn k ![_V](rmcv.gif) ![(](lp.gif)
∼ Nn ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 28, 40 | mpbiran2 885 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ∼ Nn k ![_V](rmcv.gif)
∼ Nn ![)](rp.gif) |
42 | 39, 41 | anbi12i 678 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) k ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ∼ Nn ![)](rp.gif) ![)](rp.gif) |
43 | 37, 42 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ∼ Nn ![)](rp.gif) ![)](rp.gif) |
44 | 36, 43 | orbi12i 507 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c Nn ![(](lp.gif) ∼ Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 26, 44 | bitri 240 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c Nn ![(](lp.gif) ∼ Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 25, 45 | bitr4i 243 |
. . . 4
![(](lp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 46 | rexbii 2639 |
. . 3
![(](lp.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![E.](exists.gif) ![<<](llangle.gif) ![y](_y.gif)
![x](_x.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
48 | | eqeq1 2359 |
. . . . 5
![(](lp.gif) ![(](lp.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 48 | rexbidv 2635 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | | df-phi 4565 |
. . . 4
Phi ![{](lbrace.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![}](rbrace.gif) |
51 | 28, 49, 50 | elab2 2988 |
. . 3
![(](lp.gif) Phi ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 28 | elimak 4259 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![A](_ca.gif) ![E.](exists.gif) ![<<](llangle.gif) ![y](_y.gif)
![x](_x.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 47, 51, 52 | 3bitr4i 268 |
. 2
![(](lp.gif) Phi ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
54 | 53 | eqriv 2350 |
1
Phi ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![A](_ca.gif) ![)](rp.gif) |