Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexlimivv | Unicode version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.) |
Ref | Expression |
---|---|
rexlimivv.1 |
Ref | Expression |
---|---|
rexlimivv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimivv.1 | . . 3 | |
2 | 1 | rexlimdva 2574 | . 2 |
3 | 2 | rexlimiv 2568 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 2128 wrex 2436 |
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 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-17 1506 ax-ial 1514 ax-i5r 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-ral 2440 df-rex 2441 |
This theorem is referenced by: opelxp 4617 f1o2ndf1 6176 xpdom2 6777 distrlem5prl 7507 distrlem5pru 7508 mulid1 7876 cnegex 8054 recexap 8528 creur 8831 creui 8832 cju 8833 elz2 9236 qre 9535 qaddcl 9545 qnegcl 9546 qmulcl 9547 qreccl 9552 elpqb 9559 replim 10763 prodmodc 11479 odd2np1 11768 opoe 11790 omoe 11791 opeo 11792 omeo 11793 qredeu 11978 pythagtriplem1 12144 txuni2 12698 blssioo 12987 tgioo 12988 |
Copyright terms: Public domain | W3C validator |