![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2rexbidv | Unicode version |
Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2ralbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2rexbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rexbidv 2491 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexbidv 2491 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-rex 2474 |
This theorem is referenced by: f1oiso 5848 elrnmpog 6010 elrnmpo 6011 ralrnmpo 6012 rexrnmpo 6013 ovelrn 6046 eroveu 6653 genipv 7539 genpelxp 7541 genpelvl 7542 genpelvu 7543 axcnre 7911 apreap 8575 apreim 8591 aprcl 8634 aptap 8638 bezoutlemnewy 12032 bezoutlema 12035 bezoutlemb 12036 pythagtriplem19 12317 pceu 12330 pcval 12331 pczpre 12332 pcdiv 12337 4sqlem2 12424 4sqlem3 12425 4sqlem4 12427 4sqexercise2 12434 4sqlemsdc 12435 4sq 12445 txuni2 14233 txbas 14235 txdis1cn 14255 2sqlem2 14940 2sqlem8 14948 2sqlem9 14949 |
Copyright terms: Public domain | W3C validator |