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 2471 | . 2 |
3 | 2 | rexbidv 2471 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wrex 2449 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-rex 2454 |
This theorem is referenced by: f1oiso 5803 elrnmpog 5963 elrnmpo 5964 ralrnmpo 5965 rexrnmpo 5966 ovelrn 5999 eroveu 6601 genipv 7460 genpelxp 7462 genpelvl 7463 genpelvu 7464 axcnre 7832 apreap 8495 apreim 8511 aprcl 8554 bezoutlemnewy 11940 bezoutlema 11943 bezoutlemb 11944 pythagtriplem19 12225 pceu 12238 pcval 12239 pczpre 12240 pcdiv 12245 4sqlem2 12330 4sqlem3 12331 4sqlem4 12333 txuni2 13011 txbas 13013 txdis1cn 13033 2sqlem2 13706 2sqlem8 13714 2sqlem9 13715 |
Copyright terms: Public domain | W3C validator |