Step | Hyp | Ref
| Expression |
1 | | df-sfin 4446 |
. . 3
Sfin Nn Nn 1
|
2 | | 3simpa 952 |
. . 3
Nn Nn 1
Nn Nn |
3 | 1, 2 | sylbi 187 |
. 2
Sfin Nn Nn |
4 | | sfintfinlem1 4531 |
. . . 4
Sfin Sfin Tfin
Tfin |
5 | | sfineq1 4526 |
. . . . . 6
0c Sfin
Sfin 0c |
6 | | tfineq 4488 |
. . . . . . . 8
0c Tfin Tfin
0c |
7 | | tfin0c 4497 |
. . . . . . . 8
Tfin 0c 0c |
8 | 6, 7 | syl6eq 2401 |
. . . . . . 7
0c Tfin 0c |
9 | | sfineq1 4526 |
. . . . . . 7
Tfin
0c Sfin Tfin Tfin
Sfin 0c Tfin |
10 | 8, 9 | syl 15 |
. . . . . 6
0c Sfin Tfin
Tfin Sfin 0c Tfin |
11 | 5, 10 | imbi12d 311 |
. . . . 5
0c Sfin Sfin Tfin
Tfin Sfin 0c Sfin 0c Tfin |
12 | 11 | albidv 1625 |
. . . 4
0c Sfin
Sfin Tfin Tfin
Sfin 0c Sfin 0c Tfin |
13 | | sfineq1 4526 |
. . . . . . 7
Sfin Sfin |
14 | | tfineq 4488 |
. . . . . . . 8
Tfin
Tfin |
15 | | sfineq1 4526 |
. . . . . . . 8
Tfin
Tfin Sfin Tfin
Tfin Sfin Tfin
Tfin |
16 | 14, 15 | syl 15 |
. . . . . . 7
Sfin Tfin Tfin
Sfin Tfin Tfin |
17 | 13, 16 | imbi12d 311 |
. . . . . 6
Sfin Sfin
Tfin
Tfin Sfin Sfin Tfin
Tfin |
18 | 17 | albidv 1625 |
. . . . 5
Sfin Sfin Tfin
Tfin Sfin Sfin
Tfin
Tfin |
19 | | sfineq2 4527 |
. . . . . . 7
Sfin Sfin |
20 | | tfineq 4488 |
. . . . . . . 8
Tfin
Tfin |
21 | | sfineq2 4527 |
. . . . . . . 8
Tfin
Tfin Sfin Tfin
Tfin Sfin Tfin
Tfin |
22 | 20, 21 | syl 15 |
. . . . . . 7
Sfin Tfin Tfin
Sfin Tfin
Tfin |
23 | 19, 22 | imbi12d 311 |
. . . . . 6
Sfin Sfin
Tfin
Tfin Sfin Sfin Tfin
Tfin |
24 | 23 | cbvalv 2002 |
. . . . 5
Sfin Sfin Tfin
Tfin Sfin Sfin
Tfin
Tfin |
25 | 18, 24 | syl6bb 252 |
. . . 4
Sfin Sfin Tfin
Tfin Sfin Sfin
Tfin
Tfin |
26 | | sfineq1 4526 |
. . . . . 6
1c Sfin
Sfin
1c |
27 | | tfineq 4488 |
. . . . . . 7
1c Tfin Tfin
1c |
28 | | sfineq1 4526 |
. . . . . . 7
Tfin
Tfin
1c
Sfin Tfin Tfin
Sfin Tfin 1c
Tfin |
29 | 27, 28 | syl 15 |
. . . . . 6
1c Sfin Tfin
Tfin Sfin Tfin
1c Tfin |
30 | 26, 29 | imbi12d 311 |
. . . . 5
1c Sfin Sfin Tfin
Tfin Sfin
1c Sfin Tfin
1c Tfin |
31 | 30 | albidv 1625 |
. . . 4
1c Sfin
Sfin Tfin Tfin
Sfin
1c Sfin Tfin
1c Tfin |
32 | | sfineq1 4526 |
. . . . . 6
Sfin Sfin |
33 | | tfineq 4488 |
. . . . . . 7
Tfin
Tfin |
34 | | sfineq1 4526 |
. . . . . . 7
Tfin
Tfin Sfin Tfin
Tfin Sfin Tfin
Tfin |
35 | 33, 34 | syl 15 |
. . . . . 6
Sfin Tfin Tfin
Sfin Tfin Tfin |
36 | 32, 35 | imbi12d 311 |
. . . . 5
Sfin Sfin
Tfin
Tfin Sfin Sfin Tfin
Tfin |
37 | 36 | albidv 1625 |
. . . 4
Sfin Sfin Tfin
Tfin Sfin Sfin
Tfin
Tfin |
38 | | sfin01 4528 |
. . . . . . 7
Sfin 0c 1c |
39 | | sfin112 4529 |
. . . . . . 7
Sfin
0c Sfin 0c 1c
1c |
40 | 38, 39 | mpan2 652 |
. . . . . 6
Sfin 0c 1c |
41 | | tfineq 4488 |
. . . . . . . . 9
1c Tfin Tfin
1c |
42 | | tfin1c 4499 |
. . . . . . . . 9
Tfin 1c 1c |
43 | 41, 42 | syl6eq 2401 |
. . . . . . . 8
1c Tfin 1c |
44 | | sfineq2 4527 |
. . . . . . . 8
Tfin
1c Sfin 0c Tfin Sfin 0c 1c |
45 | 43, 44 | syl 15 |
. . . . . . 7
1c Sfin 0c Tfin
Sfin 0c 1c |
46 | 38, 45 | mpbiri 224 |
. . . . . 6
1c Sfin 0c Tfin |
47 | 40, 46 | syl 15 |
. . . . 5
Sfin 0c Sfin 0c Tfin |
48 | 47 | ax-gen 1546 |
. . . 4
Sfin 0c Sfin 0c Tfin |
49 | | df-sfin 4446 |
. . . . . . . . . 10
Sfin
1c 1c Nn
Nn 1
1c |
50 | 49 | simp3bi 972 |
. . . . . . . . 9
Sfin
1c 1
1c |
51 | 50 | 3ad2ant3 978 |
. . . . . . . 8
Nn Sfin
Sfin Tfin Tfin Sfin
1c 1
1c |
52 | | sfindbl 4530 |
. . . . . . . . . . . . 13
Nn 1
1c
Nn Sfin
Sfin
1c |
53 | 52 | 3ad2antl1 1117 |
. . . . . . . . . . . 12
Nn Sfin
Sfin Tfin Tfin Sfin
1c 1
1c
Nn Sfin
Sfin
1c |
54 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . 22
Sfin Sfin |
55 | | tfineq 4488 |
. . . . . . . . . . . . . . . . . . . . . . 23
Tfin
Tfin |
56 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . . 23
Tfin
Tfin Sfin Tfin
Tfin Sfin Tfin
Tfin |
57 | 55, 56 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . 22
Sfin Tfin Tfin
Sfin Tfin
Tfin |
58 | 54, 57 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . 21
Sfin Sfin
Tfin
Tfin Sfin Sfin Tfin
Tfin |
59 | 58 | spv 1998 |
. . . . . . . . . . . . . . . . . . . 20
Sfin Sfin Tfin
Tfin Sfin Sfin Tfin
Tfin |
60 | | simprrl 740 |
. . . . . . . . . . . . . . . . . . . . . 22
Sfin
1c Nn Sfin Sfin
1c Sfin |
61 | 60 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . 21
Nn Sfin
1c Nn Sfin Sfin
1c Sfin
|
62 | | simplrl 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Sfin
1c |
63 | | simprrr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Sfin
1c Nn Sfin Sfin
1c Sfin
1c |
64 | 63 | ad2antlr 707 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Sfin
1c |
65 | | sfin112 4529 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Sfin
1c Sfin
1c |
66 | 62, 64, 65 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin |
67 | | df-sfin 4446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Sfin
1c
1c
Nn
Nn 1
1c |
68 | 67 | simp3bi 972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Sfin
1c 1
1c
|
69 | 64, 68 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin 1
1c |
70 | | simp2 956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c Sfin Tfin Tfin |
71 | | df-sfin 4446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Sfin Tfin Tfin
Tfin
Nn Tfin Nn 1
Tfin Tfin
|
72 | 71 | simp1bi 970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Sfin Tfin Tfin
Tfin
Nn |
73 | 70, 72 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c Tfin
Nn |
74 | | simp1l 979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c Nn |
75 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Nn
1c
Nn |
76 | 74, 75 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c 1c Nn |
77 | | simp3 957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c 1 1c |
78 | | tfinpw1 4494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
1c
Nn 1
1c 1 1 Tfin 1c |
79 | 76, 77, 78 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c 1 1 Tfin 1c |
80 | | ne0i 3556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
1
1c 1c |
81 | 80 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c 1c |
82 | | tfinsuc 4498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Nn 1c Tfin
1c
Tfin 1c |
83 | 74, 81, 82 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c Tfin
1c
Tfin 1c |
84 | 79, 83 | eleqtrd 2429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c 1 1 Tfin 1c |
85 | | sfindbl 4530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Tfin
Nn 1 1 Tfin 1c
Nn Sfin Tfin
Sfin Tfin
1c |
86 | 73, 84, 85 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c
Nn Sfin Tfin
Sfin Tfin
1c |
87 | | simp2 956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
Sfin Tfin
Sfin
Tfin 1c
Sfin Tfin Tfin |
88 | | simp3l 983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
Sfin Tfin
Sfin
Tfin 1c
Sfin Tfin |
89 | | sfin112 4529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Sfin
Tfin
Tfin Sfin Tfin Tfin
|
90 | 87, 88, 89 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
Sfin Tfin
Sfin
Tfin 1c
Tfin
|
91 | | addceq12 4385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
Tfin
Tfin Tfin Tfin
|
92 | 91 | anidms 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
Tfin
Tfin Tfin
|
93 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
Tfin
Tfin
Sfin Tfin
1c
Tfin Tfin Sfin Tfin 1c |
94 | 92, 93 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
Tfin
Sfin Tfin
1c
Tfin Tfin Sfin Tfin 1c |
95 | 94 | biimprcd 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
Sfin
Tfin 1c
Tfin Sfin
Tfin 1c
Tfin Tfin |
96 | 95 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Sfin
Tfin
Sfin Tfin
1c Tfin
Sfin
Tfin 1c
Tfin Tfin |
97 | 96 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
Sfin Tfin
Sfin
Tfin 1c
Tfin
Sfin
Tfin 1c
Tfin Tfin |
98 | 90, 97 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
Sfin Tfin
Sfin
Tfin 1c
Sfin
Tfin 1c
Tfin Tfin |
99 | 98 | 3expia 1153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Sfin Tfin
Sfin Tfin
1c Sfin
Tfin 1c
Tfin Tfin |
100 | 99 | rexlimdvw 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
Nn Sfin Tfin
Sfin Tfin
1c Sfin
Tfin 1c
Tfin Tfin |
101 | 100 | 3adant3 975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c
Nn Sfin Tfin
Sfin Tfin
1c Sfin
Tfin 1c
Tfin Tfin |
102 | 86, 101 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
1
1c Sfin
Tfin 1c
Tfin Tfin |
103 | 102 | 3expia 1153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin 1 1c Sfin Tfin 1c
Tfin Tfin |
104 | 103 | adantrd 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin 1
1c
Sfin
Tfin 1c
Tfin Tfin |
105 | 104 | exlimdv 1636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin 1
1c
Sfin
Tfin 1c
Tfin Tfin |
106 | 69, 105 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Sfin
Tfin 1c
Tfin Tfin |
107 | | simpll 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Nn |
108 | 80 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1
1c
1c |
109 | 108 | exlimiv 1634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1
1c
1c |
110 | 64, 68, 109 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin 1c |
111 | 107, 110,
82 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Tfin
1c
Tfin 1c |
112 | | simprrl 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Nn Sfin
1c Nn Sfin Sfin
1c
Nn |
113 | 112 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Nn |
114 | | ne0i 3556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
115 | 114 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1
1c
|
116 | 115 | exlimiv 1634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1
1c
|
117 | 64, 68, 116 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin |
118 | | tfindi 4496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nn Nn
Tfin Tfin
Tfin |
119 | 113, 113,
117, 118 | syl3anc 1182 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Tfin
Tfin Tfin |
120 | | sfineq1 4526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Tfin
1c
Tfin 1c Sfin Tfin 1c
Tfin Sfin Tfin 1c Tfin |
121 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Tfin
Tfin Tfin Sfin
Tfin 1c
Tfin Sfin Tfin 1c
Tfin Tfin |
122 | 120, 121 | sylan9bb 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Tfin
1c
Tfin 1c Tfin
Tfin Tfin
Sfin Tfin 1c
Tfin Sfin Tfin 1c
Tfin Tfin |
123 | 111, 119,
122 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Sfin Tfin 1c
Tfin Sfin Tfin 1c
Tfin Tfin |
124 | 106, 123 | mpbird 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Sfin Tfin 1c
Tfin |
125 | | tfineq 4488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Tfin
Tfin |
126 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Tfin
Tfin Sfin Tfin
1c Tfin
Sfin Tfin
1c
Tfin |
127 | 125, 126 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Sfin Tfin 1c
Tfin Sfin Tfin
1c Tfin
|
128 | 127 | biimprcd 216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Sfin Tfin 1c
Tfin
Sfin Tfin 1c
Tfin |
129 | 124, 128 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin
Sfin Tfin 1c
Tfin |
130 | 66, 129 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . 22
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin Tfin Sfin Tfin 1c
Tfin |
131 | 130 | ex 423 |
. . . . . . . . . . . . . . . . . . . . 21
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Tfin
Tfin Sfin Tfin 1c
Tfin |
132 | 61, 131 | embantd 50 |
. . . . . . . . . . . . . . . . . . . 20
Nn Sfin
1c Nn Sfin Sfin
1c
Sfin Sfin Tfin
Tfin Sfin Tfin 1c
Tfin |
133 | 59, 132 | syl5 28 |
. . . . . . . . . . . . . . . . . . 19
Nn Sfin
1c Nn Sfin Sfin
1c Sfin Sfin Tfin
Tfin Sfin Tfin 1c
Tfin |
134 | 133 | exp32 588 |
. . . . . . . . . . . . . . . . . 18
Nn Sfin
1c Nn Sfin Sfin
1c
Sfin Sfin Tfin
Tfin Sfin Tfin 1c
Tfin |
135 | 134 | com34 77 |
. . . . . . . . . . . . . . . . 17
Nn Sfin
1c Sfin
Sfin Tfin Tfin
Nn Sfin Sfin
1c Sfin Tfin 1c
Tfin |
136 | 135 | com23 72 |
. . . . . . . . . . . . . . . 16
Nn Sfin
Sfin Tfin Tfin Sfin
1c Nn Sfin Sfin
1c Sfin Tfin 1c
Tfin |
137 | 136 | 3imp 1145 |
. . . . . . . . . . . . . . 15
Nn Sfin
Sfin Tfin Tfin Sfin
1c Nn Sfin Sfin
1c Sfin Tfin 1c
Tfin |
138 | 137 | exp3a 425 |
. . . . . . . . . . . . . 14
Nn Sfin
Sfin Tfin Tfin Sfin
1c Nn Sfin Sfin
1c Sfin Tfin
1c Tfin |
139 | 138 | rexlimdv 2737 |
. . . . . . . . . . . . 13
Nn Sfin
Sfin Tfin Tfin Sfin
1c
Nn Sfin
Sfin
1c Sfin Tfin
1c Tfin |
140 | 139 | adantr 451 |
. . . . . . . . . . . 12
Nn Sfin
Sfin Tfin Tfin Sfin
1c 1
1c
Nn Sfin
Sfin
1c Sfin Tfin
1c Tfin |
141 | 53, 140 | mpd 14 |
. . . . . . . . . . 11
Nn Sfin
Sfin Tfin Tfin Sfin
1c 1
1c Sfin Tfin 1c
Tfin |
142 | 141 | ex 423 |
. . . . . . . . . 10
Nn Sfin
Sfin Tfin Tfin Sfin
1c 1
1c Sfin Tfin
1c Tfin |
143 | 142 | adantrd 454 |
. . . . . . . . 9
Nn Sfin
Sfin Tfin Tfin Sfin
1c 1
1c Sfin Tfin 1c
Tfin |
144 | 143 | exlimdv 1636 |
. . . . . . . 8
Nn Sfin
Sfin Tfin Tfin Sfin
1c 1
1c Sfin Tfin 1c
Tfin |
145 | 51, 144 | mpd 14 |
. . . . . . 7
Nn Sfin
Sfin Tfin Tfin Sfin
1c Sfin Tfin 1c
Tfin |
146 | 145 | 3expia 1153 |
. . . . . 6
Nn Sfin
Sfin Tfin Tfin Sfin
1c Sfin Tfin
1c Tfin |
147 | 146 | alrimiv 1631 |
. . . . 5
Nn Sfin
Sfin Tfin Tfin Sfin
1c Sfin Tfin
1c Tfin |
148 | 147 | ex 423 |
. . . 4
Nn Sfin
Sfin Tfin Tfin
Sfin
1c Sfin Tfin
1c Tfin |
149 | 4, 12, 25, 31, 37, 48, 148 | finds 4411 |
. . 3
Nn Sfin Sfin Tfin
Tfin |
150 | | sfineq2 4527 |
. . . . 5
Sfin Sfin |
151 | | tfineq 4488 |
. . . . . 6
Tfin
Tfin |
152 | | sfineq2 4527 |
. . . . . 6
Tfin
Tfin Sfin Tfin
Tfin Sfin Tfin
Tfin |
153 | 151, 152 | syl 15 |
. . . . 5
Sfin Tfin Tfin
Sfin Tfin
Tfin |
154 | 150, 153 | imbi12d 311 |
. . . 4
Sfin Sfin
Tfin
Tfin Sfin Sfin Tfin
Tfin |
155 | 154 | spcgv 2939 |
. . 3
Nn Sfin
Sfin Tfin Tfin Sfin Sfin Tfin
Tfin |
156 | 149, 155 | mpan9 455 |
. 2
Nn Nn Sfin Sfin Tfin
Tfin |
157 | 3, 156 | mpcom 32 |
1
Sfin Sfin Tfin
Tfin |