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 2481 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 wral 2393 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-ral 2398 |
This theorem is referenced by: r19.27v 2536 r19.28v 2537 exse 4228 sosng 4582 dmxpm 4729 exse2 4883 funco 5133 acexmidlemph 5735 mpoeq12 5799 xpexgALT 5999 mpoexg 6077 rdgtfr 6239 rdgruledefgg 6240 rdgivallem 6246 frecabex 6263 frectfr 6265 omfnex 6313 oeiv 6320 uniqs 6455 sbthlemi5 6817 sbthlemi6 6818 updjud 6935 exmidfodomrlemim 7025 exmidaclem 7032 genpdisj 7299 ltexprlemloc 7383 recexprlemloc 7407 cauappcvgprlemrnd 7426 cauappcvgprlemdisj 7427 caucvgprlemrnd 7449 caucvgprlemdisj 7450 caucvgprprlemrnd 7477 caucvgprprlemdisj 7478 suplocexpr 7501 recan 10849 climconst 11027 sumeq2ad 11106 dvdsext 11480 neif 12237 lmconst 12312 cndis 12337 |
Copyright terms: Public domain | W3C validator |