![]() |
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 2457 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-4 1452 ax-17 1471 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-ral 2375 |
This theorem is referenced by: exse 4187 sosng 4540 dmxpm 4687 exse2 4839 funco 5088 acexmidlemph 5683 mpt2eq12 5747 xpexgALT 5942 mpt2exg 6016 rdgtfr 6177 rdgruledefgg 6178 rdgivallem 6184 frecabex 6201 frectfr 6203 omfnex 6250 oeiv 6257 uniqs 6390 sbthlemi5 6750 sbthlemi6 6751 updjud 6853 exmidfodomrlemim 6924 genpdisj 7179 ltexprlemloc 7263 recexprlemloc 7287 cauappcvgprlemrnd 7306 cauappcvgprlemdisj 7307 caucvgprlemrnd 7329 caucvgprlemdisj 7330 caucvgprprlemrnd 7357 caucvgprprlemdisj 7358 recan 10657 climconst 10833 sumeq2ad 10912 dvdsext 11283 neif 11993 lmconst 12067 cndis 12092 |
Copyright terms: Public domain | W3C validator |