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 2509 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1480 wral 2414 |
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-4 1487 ax-17 1506 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-ral 2419 |
This theorem is referenced by: ralxfrd 4378 isoselem 5714 isosolem 5718 findcard 6775 nnsub 8752 supinfneg 9383 infsupneg 9384 ublbneg 9398 expnlbnd2 10410 cau3lem 10879 climshftlemg 11064 subcn2 11073 serf0 11114 sqrt2irr 11829 tgcn 12366 tgcnp 12367 lmconst 12374 cnntr 12383 lmss 12404 txdis 12435 txlm 12437 blbas 12591 metss 12652 metcnp3 12669 |
Copyright terms: Public domain | W3C validator |