Step | Hyp | Ref
| Expression |
1 | | tfinnnul 4490 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) Tfin ![(/)](varnothing.gif) ![)](rp.gif) |
2 | 1 | ex 423 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) Tfin ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
3 | 2 | adantrd 454 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif)
Tfin ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 3 | adantr 451 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif)
Tfin ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | addcnul1 4452 |
. . . . . . . . . . . . . 14
1c ![(/)](varnothing.gif) ![(/)](varnothing.gif) |
6 | | addccom 4406 |
. . . . . . . . . . . . . 14
1c ![(/)](varnothing.gif) ![(](lp.gif)
1c![)](rp.gif) |
7 | 5, 6 | eqtr3i 2375 |
. . . . . . . . . . . . 13
![(](lp.gif) 1c![)](rp.gif) |
8 | | addceq2 4384 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif)
Tfin ![y](_y.gif) Tfin ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | addcnul1 4452 |
. . . . . . . . . . . . . . . . 17
Tfin ![(/)](varnothing.gif) ![(/)](varnothing.gif) |
10 | 8, 9 | syl6eq 2401 |
. . . . . . . . . . . . . . . 16
![(](lp.gif)
Tfin ![y](_y.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
11 | 10 | addceq1d 4389 |
. . . . . . . . . . . . . . 15
![(](lp.gif)
![(](lp.gif) Tfin ![y](_y.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
12 | 11 | eqeq2d 2364 |
. . . . . . . . . . . . . 14
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) Tfin ![y](_y.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | rspcev 2955 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
14 | 7, 13 | mpan2 652 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![E.](exists.gif) Nn ![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
15 | | eleq1 2413 |
. . . . . . . . . . . . 13
![(](lp.gif)
![(](lp.gif)
Nn Nn ![)](rp.gif) ![)](rp.gif) |
16 | | tfineq 4488 |
. . . . . . . . . . . . . . . 16
![(](lp.gif)
Tfin
Tfin ![(/)](varnothing.gif) ![)](rp.gif) |
17 | | tfinnul 4491 |
. . . . . . . . . . . . . . . 16
Tfin ![(/)](varnothing.gif) |
18 | 16, 17 | syl6eq 2401 |
. . . . . . . . . . . . . . 15
![(](lp.gif)
Tfin
![(/)](varnothing.gif) ![)](rp.gif) |
19 | 18 | eqeq1d 2361 |
. . . . . . . . . . . . . 14
![(](lp.gif)
Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c ![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | rexbidv 2635 |
. . . . . . . . . . . . 13
![(](lp.gif)
![(](lp.gif) ![E.](exists.gif)
Nn Tfin ![(](lp.gif)
Tfin ![y](_y.gif)
1c
![E.](exists.gif) Nn ![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 15, 20 | imbi12d 311 |
. . . . . . . . . . . 12
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
Nn ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![(](lp.gif)
Nn ![E.](exists.gif) Nn ![(](lp.gif) Tfin ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 14, 21 | mpbiri 224 |
. . . . . . . . . . 11
![(](lp.gif)
![(](lp.gif)
Nn ![E.](exists.gif) Nn Tfin ![(](lp.gif)
Tfin ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | adantld 453 |
. . . . . . . . . 10
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
Nn Nn ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | adantrd 454 |
. . . . . . . . 9
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![)](rp.gif) ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | a1dd 42 |
. . . . . . . 8
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | simp2r 982 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif)
Nn ![)](rp.gif) |
27 | | simp3r 984 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
28 | | simp3l 983 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
29 | 27, 28 | eqnetrrd 2536 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
30 | | addcnnul 4453 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![(](lp.gif) ![(](lp.gif)
![x](_x.gif)
1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 29, 30 | syl 15 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 31 | simpld 445 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![x](_x.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
33 | | addcnnul 4453 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 32, 33 | syl 15 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | simprd 449 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
36 | | tfinprop 4489 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) Tfin Nn ![E.](exists.gif) 1 Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | simpld 445 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) Tfin Nn ![)](rp.gif) |
38 | 26, 35, 37 | syl2anc 642 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) Tfin
Nn ![)](rp.gif) |
39 | | tfineq 4488 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
Tfin
Tfin ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
40 | 39 | adantl 452 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) Tfin
Tfin ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
41 | 40 | 3ad2ant3 978 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) Tfin
Tfin ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
42 | | simp1l 979 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif)
Nn ![)](rp.gif) |
43 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![x](_x.gif) Nn ![)](rp.gif) |
44 | 42, 26, 43 | syl2anc 642 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![x](_x.gif)
Nn ![)](rp.gif) |
45 | | tfinsuc 4498 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![(/)](varnothing.gif) Tfin ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c
Tfin ![(](lp.gif)
![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
46 | 44, 29, 45 | syl2anc 642 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) Tfin
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c
Tfin ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
47 | 41, 46 | eqtrd 2385 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) Tfin
Tfin ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) |
48 | | tfindi 4496 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![x](_x.gif)
![(/)](varnothing.gif) Tfin ![(](lp.gif) ![x](_x.gif) Tfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 42, 26, 32, 48 | syl3anc 1182 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) Tfin
![(](lp.gif) ![x](_x.gif) Tfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 49 | addceq1d 4389 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) Tfin ![(](lp.gif) ![x](_x.gif)
1c
![(](lp.gif) Tfin Tfin ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) |
51 | 47, 50 | eqtrd 2385 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) Tfin
![(](lp.gif)
Tfin Tfin ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
52 | | addceq2 4384 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Tfin Tfin ![y](_y.gif) Tfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 52 | addceq1d 4389 |
. . . . . . . . . . . . . 14
![(](lp.gif) Tfin ![(](lp.gif) Tfin ![y](_y.gif) 1c ![(](lp.gif) Tfin Tfin ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
54 | 53 | eqeq2d 2364 |
. . . . . . . . . . . . 13
![(](lp.gif) Tfin Tfin ![(](lp.gif) Tfin ![y](_y.gif) 1c Tfin
![(](lp.gif) Tfin Tfin ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 54 | rspcev 2955 |
. . . . . . . . . . . 12
![(](lp.gif) Tfin
Nn Tfin
![(](lp.gif) Tfin Tfin ![x](_x.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn Tfin
![(](lp.gif)
Tfin ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) |
56 | 38, 51, 55 | syl2anc 642 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Nn Tfin ![(](lp.gif)
Tfin ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) |
57 | 56 | 3expa 1151 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) Nn ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Nn Tfin ![(](lp.gif)
Tfin ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) |
58 | 57 | exp32 588 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![)](rp.gif) ![(](lp.gif)
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![E.](exists.gif) Nn Tfin ![(](lp.gif)
Tfin ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 58 | com12 27 |
. . . . . . . 8
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 25, 59 | pm2.61ine 2592 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
61 | 60 | expr 598 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
62 | 61 | rexlimdv 2737 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
63 | 62 | ex 423 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif)
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 63 | imp3a 420 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif)
![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 4, 64 | jcad 519 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif)
Tfin
![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
66 | | opkltfing 4449 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
67 | | tfinex 4485 |
. . . 4
Tfin
![_V](rmcv.gif) |
68 | | tfinex 4485 |
. . . 4
Tfin
![_V](rmcv.gif) |
69 | | opkltfing 4449 |
. . . 4
![(](lp.gif) Tfin
Tfin ![_V](rmcv.gif) ![(](lp.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin Tfin
![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
70 | 67, 68, 69 | mp2an 653 |
. . 3
![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin Tfin ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
71 | 70 | a1i 10 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin Tfin ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
72 | 65, 66, 71 | 3imtr4d 259 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |