Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > spc2gv | Unicode version |
Description: Specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.) |
Ref | Expression |
---|---|
spc2egv.1 |
Ref | Expression |
---|---|
spc2gv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2749 | . . . 4 | |
2 | elisset 2749 | . . . 4 | |
3 | 1, 2 | anim12i 338 | . . 3 |
4 | eeanv 1930 | . . 3 | |
5 | 3, 4 | sylibr 134 | . 2 |
6 | spc2egv.1 | . . . . . 6 | |
7 | 6 | biimpcd 159 | . . . . 5 |
8 | 7 | 2alimi 1454 | . . . 4 |
9 | exim 1597 | . . . . 5 | |
10 | 9 | alimi 1453 | . . . 4 |
11 | exim 1597 | . . . 4 | |
12 | 8, 10, 11 | 3syl 17 | . . 3 |
13 | 19.9v 1869 | . . . 4 | |
14 | 19.9v 1869 | . . . 4 | |
15 | 13, 14 | bitri 184 | . . 3 |
16 | 12, 15 | syl6ib 161 | . 2 |
17 | 5, 16 | syl5com 29 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 104 wb 105 wal 1351 wceq 1353 wex 1490 wcel 2146 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-ext 2157 |
This theorem depends on definitions: df-bi 117 df-nf 1459 df-sb 1761 df-clab 2162 df-cleq 2168 df-clel 2171 df-v 2737 |
This theorem is referenced by: rspc2gv 2851 trel 4103 exmidundif 4201 exmidundifim 4202 elovmpo 6062 cnmpt12 13280 cnmpt22 13287 exmidsbthrlem 14253 |
Copyright terms: Public domain | W3C validator |