Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralrimdva | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) |
Ref | Expression |
---|---|
ralrimdva.1 |
Ref | Expression |
---|---|
ralrimdva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimdva.1 | . . . 4 | |
2 | 1 | ex 114 | . . 3 |
3 | 2 | com23 78 | . 2 |
4 | 3 | ralrimdv 2543 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 2135 wral 2442 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-ral 2447 |
This theorem is referenced by: ralxfrd 4434 isoselem 5782 isosolem 5786 findcard 6845 nnsub 8887 supinfneg 9524 infsupneg 9525 ublbneg 9542 expnlbnd2 10569 cau3lem 11042 climshftlemg 11229 subcn2 11238 serf0 11279 sqrt2irr 12073 pclemub 12198 prmpwdvds 12264 tgcn 12755 tgcnp 12756 lmconst 12763 cnntr 12772 lmss 12793 txdis 12824 txlm 12826 blbas 12980 metss 13041 metcnp3 13058 iswomni0 13771 |
Copyright terms: Public domain | W3C validator |