![]() |
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 2385 |
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 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-ral 2305 |
This theorem is referenced by: exse 4058 sosng 4356 dmxpm 4498 exse2 4642 funco 4883 acexmidlemph 5448 mpt2eq12 5507 xpexgALT 5702 mpt2exg 5776 rdgtfr 5901 rdgruledefgg 5902 rdgivallem 5908 frecabex 5923 frectfr 5924 omfnex 5968 oeiv 5975 oeicl 5981 uniqs 6100 genpdisj 6506 ltexprlemloc 6581 recexprlemloc 6603 cauappcvgprlemrnd 6622 cauappcvgprlemdisj 6623 caucvgprlemrnd 6644 caucvgprlemdisj 6645 |
Copyright terms: Public domain | W3C validator |