![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralrimiv | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
ralrimiv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralrimiv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1466 |
. 2
![]() ![]() ![]() ![]() | |
2 | ralrimiv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralrimi 2444 |
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 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-4 1445 ax-17 1464 |
This theorem depends on definitions: df-bi 115 df-nf 1395 df-ral 2364 |
This theorem is referenced by: ralrimiva 2446 ralrimivw 2447 ralrimivv 2454 r19.27av 2504 rr19.3v 2755 rabssdv 3101 rzal 3379 trin 3946 class2seteq 3998 ralxfrALT 4289 ssorduni 4304 ordsucim 4317 onintonm 4334 issref 4814 funimaexglem 5097 resflem 5462 poxp 5997 rdgss 6148 dom2lem 6489 supisoti 6705 ordiso2 6728 updjud 6773 uzind 8857 zindd 8864 lbzbi 9101 icoshftf1o 9408 maxabslemval 10641 fisum0diag2 10841 alzdvds 11133 hashgcdeq 11482 bj-nntrans2 11847 bj-inf2vnlem1 11865 |
Copyright terms: Public domain | W3C validator |