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 2436 | . 2 |
3 | 2 | rexbidv 2436 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wrex 2415 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-rex 2420 |
This theorem is referenced by: f1oiso 5720 elrnmpog 5876 elrnmpo 5877 ralrnmpo 5878 rexrnmpo 5879 ovelrn 5912 eroveu 6513 genipv 7310 genpelxp 7312 genpelvl 7313 genpelvu 7314 axcnre 7682 apreap 8342 apreim 8358 aprcl 8401 bezoutlemnewy 11673 bezoutlema 11676 bezoutlemb 11677 txuni2 12414 txbas 12416 txdis1cn 12436 |
Copyright terms: Public domain | W3C validator |