Step | Hyp | Ref
| Expression |
1 | | dfrex2 2996 |
. . . . . . . . . . 11
|
2 | 1 | ralbii 2980 |
. . . . . . . . . 10
|
3 | | ralnex 2992 |
. . . . . . . . . 10
|
4 | 2, 3 | bitr2i 265 |
. . . . . . . . 9
|
5 | | elin 3796 |
. . . . . . . . . . . . . . . . . . 19
|
6 | | elpwi 4168 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
7 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
8 | | uncom 3757 |
. . . . . . . . . . . . . . . . . . . . . 22
|
9 | 7, 8 | syl6sseq 3651 |
. . . . . . . . . . . . . . . . . . . . 21
|
10 | | ssundif 4052 |
. . . . . . . . . . . . . . . . . . . . 21
|
11 | 9, 10 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
|
12 | | diffi 8192 |
. . . . . . . . . . . . . . . . . . . . 21
|
13 | 12 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
14 | 11, 13 | jca 554 |
. . . . . . . . . . . . . . . . . . 19
|
15 | 5, 14 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
|
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
17 | 16 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
|
18 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
|
19 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | elpw2 4828 |
. . . . . . . . . . . . . . . . . 18
|
21 | 20 | anbi1i 731 |
. . . . . . . . . . . . . . . . 17
|
22 | 18, 21 | bitr2i 265 |
. . . . . . . . . . . . . . . 16
|
23 | 17, 22 | sylib 208 |
. . . . . . . . . . . . . . 15
|
24 | | simprrr 805 |
. . . . . . . . . . . . . . . . 17
|
25 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . . . . 22
|
26 | 25 | simplbi2 655 |
. . . . . . . . . . . . . . . . . . . . 21
|
27 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | | orcom 402 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
29 | 27, 28 | bitr4i 267 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | | df-or 385 |
. . . . . . . . . . . . . . . . . . . . . 22
|
31 | 29, 30 | bitr2i 265 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 26, 31 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 32 | ssriv 3607 |
. . . . . . . . . . . . . . . . . . 19
|
34 | | uniss 4458 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 33, 34 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
|
36 | | uniun 4456 |
. . . . . . . . . . . . . . . . . . 19
|
37 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | 37 | unisn 4451 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 38 | uneq2i 3764 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 36, 39 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
41 | 35, 40 | syl6sseq 3651 |
. . . . . . . . . . . . . . . . 17
|
42 | 24, 41 | eqsstrd 3639 |
. . . . . . . . . . . . . . . 16
|
43 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . 21
|
44 | 43 | unissi 4461 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | | sseq2 3627 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | 44, 45 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | ad2antll 765 |
. . . . . . . . . . . . . . . . 17
|
49 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
50 | 49 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
51 | 50 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . . . . 22
|
52 | 51 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | 52 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 53, 54 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
|
56 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . 19
|
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
58 | | fibas 20781 |
. . . . . . . . . . . . . . . . . . . . 21
|
59 | | unitg 20771 |
. . . . . . . . . . . . . . . . . . . . 21
|
60 | 58, 59 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | | unieq 4444 |
. . . . . . . . . . . . . . . . . . . . . 22
|
62 | 61 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . 21
|
63 | 62 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
|
64 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
|
65 | | fiuni 8334 |
. . . . . . . . . . . . . . . . . . . . 21
|
66 | 64, 65 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | 60, 63, 66 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . . . . . 19
|
68 | | alexsubALT.1 |
. . . . . . . . . . . . . . . . . . 19
|
69 | 67, 68 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . 18
|
70 | 57, 69 | sseqtrd 3641 |
. . . . . . . . . . . . . . . . 17
|
71 | 48, 70 | unssd 3789 |
. . . . . . . . . . . . . . . 16
|
72 | 42, 71 | eqssd 3620 |
. . . . . . . . . . . . . . 15
|
73 | | unieq 4444 |
. . . . . . . . . . . . . . . . . 18
|
74 | 73 | uneq1d 3766 |
. . . . . . . . . . . . . . . . 17
|
75 | 74 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | rspcev 3309 |
. . . . . . . . . . . . . . 15
|
77 | 23, 72, 76 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
78 | 77 | expr 643 |
. . . . . . . . . . . . 13
|
79 | 78 | expd 452 |
. . . . . . . . . . . 12
|
80 | 79 | rexlimdv 3030 |
. . . . . . . . . . 11
|
81 | 80 | ralimdva 2962 |
. . . . . . . . . 10
|
82 | | inss2 3834 |
. . . . . . . . . . . . . . 15
|
83 | 82 | sseli 3599 |
. . . . . . . . . . . . . 14
|
84 | 83 | adantr 481 |
. . . . . . . . . . . . 13
|
85 | | unieq 4444 |
. . . . . . . . . . . . . . . . 17
|
86 | 85 | uneq1d 3766 |
. . . . . . . . . . . . . . . 16
|
87 | 86 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
88 | 87 | ac6sfi 8204 |
. . . . . . . . . . . . . 14
|
89 | 88 | ex 450 |
. . . . . . . . . . . . 13
|
90 | 84, 89 | syl 17 |
. . . . . . . . . . . 12
|
91 | 90 | adantr 481 |
. . . . . . . . . . 11
|
92 | 91 | ad2antrl 764 |
. . . . . . . . . 10
|
93 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . 20
|
94 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | | elpwi 4168 |
. . . . . . . . . . . . . . . . . . . . . 22
|
96 | 95 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 94, 96 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 93, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 98 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . 18
|
100 | | iunss 4561 |
. . . . . . . . . . . . . . . . . 18
|
101 | 99, 100 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
102 | 101 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
|
103 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
|
104 | 103 | snssd 4340 |
. . . . . . . . . . . . . . . 16
|
105 | 102, 104 | unssd 3789 |
. . . . . . . . . . . . . . 15
|
106 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . . . 22
|
107 | 106, 93 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . 21
|
108 | 107 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . 20
|
109 | | iunfi 8254 |
. . . . . . . . . . . . . . . . . . . 20
|
110 | 84, 108, 109 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
111 | 110 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
112 | 111 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
113 | 112 | ad2ant2lr 784 |
. . . . . . . . . . . . . . . 16
|
114 | | snfi 8038 |
. . . . . . . . . . . . . . . 16
|
115 | | unfi 8227 |
. . . . . . . . . . . . . . . 16
|
116 | 113, 114,
115 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
117 | 105, 116 | jca 554 |
. . . . . . . . . . . . . 14
|
118 | | elin 3796 |
. . . . . . . . . . . . . . 15
|
119 | 19 | elpw2 4828 |
. . . . . . . . . . . . . . . 16
|
120 | 119 | anbi1i 731 |
. . . . . . . . . . . . . . 15
|
121 | 118, 120 | bitr2i 265 |
. . . . . . . . . . . . . 14
|
122 | 117, 121 | sylib 208 |
. . . . . . . . . . . . 13
|
123 | | ralnex 2992 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
124 | 123 | imbi2i 326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
125 | 124 | albii 1747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
126 | | alinexa 1770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
127 | 125, 126 | bitr2i 265 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
128 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
129 | 128 | unieqd 4446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
130 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
131 | 129, 130 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
132 | 131 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
133 | 132 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
134 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
135 | 134 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
136 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
137 | | eluni 4439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
138 | 137 | orbi1i 542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
139 | | df-or 385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
140 | | alinexa 1770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
141 | 140 | imbi1i 339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
142 | 139, 141 | bitr4i 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
143 | 136, 138,
142 | 3bitri 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
144 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
145 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
146 | 145 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
147 | 146 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
148 | 144, 147 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
149 | 148 | spv 2260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
150 | 128 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
151 | 150 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
152 | 151 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
153 | 149, 152 | syl9r 78 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
154 | 153 | alrimdv 1857 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
155 | 154 | imim1d 82 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
156 | 143, 155 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
157 | 156 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
158 | 135, 157 | syl9r 78 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
159 | 133, 158 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
160 | 159 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
161 | 160 | imp31 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
162 | 161 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
163 | 162 | ralrimdv 2968 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
164 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
165 | 164 | elint2 4482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
166 | 163, 165 | syl6ibr 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
167 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
168 | 167 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
169 | 166, 168 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
170 | 127, 169 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . 22
|
171 | 170 | orrd 393 |
. . . . . . . . . . . . . . . . . . . . 21
|
172 | 171 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
|
173 | | orc 400 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
174 | 173 | anim2i 593 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
175 | 174 | eximi 1762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
176 | | equid 1939 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
177 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
178 | | equequ1 1952 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
179 | 144, 178 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
180 | 177, 179 | spcev 3300 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
181 | 176, 180 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
182 | | olc 399 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
183 | 182 | anim2i 593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
184 | 183 | eximi 1762 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
185 | 181, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
186 | 175, 185 | jaoi 394 |
. . . . . . . . . . . . . . . . . . . . 21
|
187 | | eluni 4439 |
. . . . . . . . . . . . . . . . . . . . . 22
|
188 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
189 | | eliun 4524 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
190 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
191 | 189, 190 | orbi12i 543 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
192 | 188, 191 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
193 | 192 | anbi2i 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
194 | 193 | exbii 1774 |
. . . . . . . . . . . . . . . . . . . . . 22
|
195 | 187, 194 | bitr2i 265 |
. . . . . . . . . . . . . . . . . . . . 21
|
196 | 186, 195 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
|
197 | 172, 196 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
|
198 | 197 | adantll 750 |
. . . . . . . . . . . . . . . . . 18
|
199 | 198 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
200 | 199 | adantlr 751 |
. . . . . . . . . . . . . . . 16
|
201 | 200 | ad2ant2l 782 |
. . . . . . . . . . . . . . 15
|
202 | 201 | ssrdv 3609 |
. . . . . . . . . . . . . 14
|
203 | | elun 3753 |
. . . . . . . . . . . . . . . . . 18
|
204 | | eliun 4524 |
. . . . . . . . . . . . . . . . . . 19
|
205 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . 19
|
206 | 204, 205 | orbi12i 543 |
. . . . . . . . . . . . . . . . . 18
|
207 | 203, 206 | bitri 264 |
. . . . . . . . . . . . . . . . 17
|
208 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . . 20
|
209 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
|
210 | | rsp 2929 |
. . . . . . . . . . . . . . . . . . . . 21
|
211 | | eqimss2 3658 |
. . . . . . . . . . . . . . . . . . . . . 22
|
212 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
213 | | ssun3 3778 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
215 | | sstr 3611 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
216 | 215 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . 22
|
217 | 211, 214,
216 | syl2im 40 |
. . . . . . . . . . . . . . . . . . . . 21
|
218 | 210, 217 | syl6 35 |
. . . . . . . . . . . . . . . . . . . 20
|
219 | 208, 209,
218 | rexlimd 3026 |
. . . . . . . . . . . . . . . . . . 19
|
220 | 219 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
|
221 | | elpwi 4168 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
222 | 221 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
223 | 222 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
224 | 223, 103 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
|
225 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . . . 21
|
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
227 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
228 | 61, 227 | syl6req 2673 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
229 | 228, 68 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . 22
|
230 | 229 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . 21
|
231 | 230 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
|
232 | 226, 231 | sseqtrd 3641 |
. . . . . . . . . . . . . . . . . . 19
|
233 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . 19
|
234 | 232, 233 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . 18
|
235 | 220, 234 | jaod 395 |
. . . . . . . . . . . . . . . . 17
|
236 | 207, 235 | syl5bi 232 |
. . . . . . . . . . . . . . . 16
|
237 | 236 | ralrimiv 2965 |
. . . . . . . . . . . . . . 15
|
238 | | unissb 4469 |
. . . . . . . . . . . . . . 15
|
239 | 237, 238 | sylibr 224 |
. . . . . . . . . . . . . 14
|
240 | 202, 239 | eqssd 3620 |
. . . . . . . . . . . . 13
|
241 | | unieq 4444 |
. . . . . . . . . . . . . . 15
|
242 | 241 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
243 | 242 | rspcev 3309 |
. . . . . . . . . . . . 13
|
244 | 122, 240,
243 | syl2anc 693 |
. . . . . . . . . . . 12
|
245 | 244 | ex 450 |
. . . . . . . . . . 11
|
246 | 245 | exlimdv 1861 |
. . . . . . . . . 10
|
247 | 81, 92, 246 | 3syld 60 |
. . . . . . . . 9
|
248 | 4, 247 | syl5bi 232 |
. . . . . . . 8
|
249 | | dfrex2 2996 |
. . . . . . . 8
|
250 | 248, 249 | syl6ib 241 |
. . . . . . 7
|
251 | 250 | con4d 114 |
. . . . . 6
|
252 | 251 | exp32 631 |
. . . . 5
|
253 | 252 | com24 95 |
. . . 4
|
254 | 253 | exp32 631 |
. . 3
|
255 | 254 | imp45 623 |
. 2
|
256 | 255 | imp31 448 |
1
|