Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralrimivw | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
ralrimivw.1 |
Ref | Expression |
---|---|
ralrimivw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimivw.1 | . . 3 | |
2 | 1 | a1d 22 | . 2 |
3 | 2 | ralrimiv 2504 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 wral 2416 |
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 2421 |
This theorem is referenced by: r19.27v 2559 r19.28v 2560 exse 4258 sosng 4612 dmxpm 4759 exse2 4913 funco 5163 acexmidlemph 5767 mpoeq12 5831 xpexgALT 6031 mpoexg 6109 rdgtfr 6271 rdgruledefgg 6272 rdgivallem 6278 frecabex 6295 frectfr 6297 omfnex 6345 oeiv 6352 uniqs 6487 sbthlemi5 6849 sbthlemi6 6850 updjud 6967 exmidfodomrlemim 7057 exmidaclem 7064 genpdisj 7331 ltexprlemloc 7415 recexprlemloc 7439 cauappcvgprlemrnd 7458 cauappcvgprlemdisj 7459 caucvgprlemrnd 7481 caucvgprlemdisj 7482 caucvgprprlemrnd 7509 caucvgprprlemdisj 7510 suplocexpr 7533 recan 10881 climconst 11059 sumeq2ad 11138 dvdsext 11553 neif 12310 lmconst 12385 cndis 12410 |
Copyright terms: Public domain | W3C validator |