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 114 | . 2 |
3 | 2 | rexlimiv 2581 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 2141 wrex 2449 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-i5r 1528 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-ral 2453 df-rex 2454 |
This theorem is referenced by: unon 4495 reg2exmidlema 4518 ssfilem 6853 diffitest 6865 fival 6947 elfi2 6949 fi0 6952 djuss 7047 updjud 7059 enumct 7092 finnum 7160 dmaddpqlem 7339 nqpi 7340 nq0nn 7404 recexprlemm 7586 rexanuz 10952 r19.2uz 10957 maxleast 11177 fsum2dlemstep 11397 fisumcom2 11401 fprod2dlemstep 11585 fprodcom2fi 11589 0dvds 11773 even2n 11833 m1expe 11858 m1exp1 11860 modprm0 12208 dfgrp2 12732 epttop 12884 neipsm 12948 tgioo 13340 sin0pilem2 13497 pilem3 13498 bj-nn0suc 13999 bj-nn0sucALT 14013 trirec0xor 14077 |
Copyright terms: Public domain | W3C validator |