Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexlimdvva | Unicode version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rexlimdvva.1 |
Ref | Expression |
---|---|
rexlimdvva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdvva.1 | . . 3 | |
2 | 1 | ex 114 | . 2 |
3 | 2 | rexlimdvv 2556 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1480 wrex 2417 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-i5r 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-ral 2421 df-rex 2422 |
This theorem is referenced by: ovelrn 5919 f1o2ndf1 6125 eroveu 6520 eroprf 6522 genipv 7317 genpelvl 7320 genpelvu 7321 genprndl 7329 genprndu 7330 addlocpr 7344 addnqprlemrl 7365 addnqprlemru 7366 mulnqprlemrl 7381 mulnqprlemru 7382 ltsopr 7404 ltaddpr 7405 ltexprlemfl 7417 ltexprlemrl 7418 ltexprlemfu 7419 ltexprlemru 7420 cauappcvgprlemladdfu 7462 cauappcvgprlemladdfl 7463 caucvgprlemdisj 7482 caucvgprlemladdfu 7485 caucvgprprlemdisj 7510 apreap 8349 apreim 8365 apirr 8367 apsym 8368 apcotr 8369 apadd1 8370 apneg 8373 mulext1 8374 apti 8384 aprcl 8408 qapne 9431 qtri3or 10020 exbtwnzlemex 10027 rebtwn2z 10032 cjap 10678 rexanre 10992 climcn2 11078 summodc 11152 prodmodclem2 11346 prodmodc 11347 eirrap 11484 dvds2lem 11505 bezoutlemnewy 11684 bezoutlembi 11693 dvdsmulgcd 11713 divgcdcoprm0 11782 cncongr1 11784 sqrt2irrap 11858 restbasg 12337 txbas 12427 blin2 12601 xmettxlem 12678 xmettx 12679 addcncntoplem 12720 mulcncf 12760 |
Copyright terms: Public domain | W3C validator |