![]() |
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 2562 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 |
This theorem is referenced by: r19.27v 2617 r19.28v 2618 exse 4351 sosng 4714 dmxpm 4862 exse2 5017 funco 5272 acexmidlemph 5885 mpoeq12 5952 xpexgALT 6153 mpoexg 6231 rdgtfr 6394 rdgruledefgg 6395 rdgivallem 6401 frecabex 6418 frectfr 6420 omfnex 6469 oeiv 6476 uniqs 6614 exmidpw2en 6935 sbthlemi5 6985 sbthlemi6 6986 updjud 7106 exmidfodomrlemim 7225 exmidaclem 7232 exmidapne 7284 cc4f 7293 genpdisj 7547 ltexprlemloc 7631 recexprlemloc 7655 cauappcvgprlemrnd 7674 cauappcvgprlemdisj 7675 caucvgprlemrnd 7697 caucvgprlemdisj 7698 caucvgprprlemrnd 7725 caucvgprprlemdisj 7726 suplocexpr 7749 recan 11145 climconst 11325 sumeq2ad 11404 dvdsext 11888 zsupssdc 11982 pc11 12358 ptex 12762 prdsex 12767 imasex 12775 imasbas 12777 imasplusg 12778 imasmulr 12779 imasaddfnlemg 12784 imasaddvallemg 12785 quslem 12794 grpinvfng 12981 scaffng 13618 neif 14078 lmconst 14153 cndis 14178 2sqlem10 14909 |
Copyright terms: Public domain | W3C validator |