![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimiva | Unicode version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) |
Ref | Expression |
---|---|
rexlimiva.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rexlimiva |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimiva.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexlimiv 2588 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-i5r 1535 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 df-rex 2461 |
This theorem is referenced by: unon 4512 reg2exmidlema 4535 ssfilem 6878 diffitest 6890 fival 6972 elfi2 6974 fi0 6977 djuss 7072 updjud 7084 enumct 7117 finnum 7185 dmaddpqlem 7379 nqpi 7380 nq0nn 7444 recexprlemm 7626 rexanuz 11000 r19.2uz 11005 maxleast 11225 fsum2dlemstep 11445 fisumcom2 11449 fprod2dlemstep 11633 fprodcom2fi 11637 0dvds 11821 even2n 11882 m1expe 11907 m1exp1 11909 modprm0 12257 dfgrp2 12910 epttop 13778 neipsm 13842 tgioo 14234 sin0pilem2 14391 pilem3 14392 bj-nn0suc 14904 bj-nn0sucALT 14918 trirec0xor 14982 |
Copyright terms: Public domain | W3C validator |