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 2533 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1465 wrex 2394 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 ax-i5r 1500 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-ral 2398 df-rex 2399 |
This theorem is referenced by: ovelrn 5887 f1o2ndf1 6093 eroveu 6488 eroprf 6490 genipv 7285 genpelvl 7288 genpelvu 7289 genprndl 7297 genprndu 7298 addlocpr 7312 addnqprlemrl 7333 addnqprlemru 7334 mulnqprlemrl 7349 mulnqprlemru 7350 ltsopr 7372 ltaddpr 7373 ltexprlemfl 7385 ltexprlemrl 7386 ltexprlemfu 7387 ltexprlemru 7388 cauappcvgprlemladdfu 7430 cauappcvgprlemladdfl 7431 caucvgprlemdisj 7450 caucvgprlemladdfu 7453 caucvgprprlemdisj 7478 apreap 8316 apreim 8332 apirr 8334 apsym 8335 apcotr 8336 apadd1 8337 apneg 8340 mulext1 8341 apti 8351 aprcl 8375 qapne 9387 qtri3or 9975 exbtwnzlemex 9982 rebtwn2z 9987 cjap 10633 rexanre 10947 climcn2 11033 summodc 11107 eirrap 11396 dvds2lem 11417 bezoutlemnewy 11596 bezoutlembi 11605 dvdsmulgcd 11625 divgcdcoprm0 11694 cncongr1 11696 sqrt2irrap 11769 restbasg 12248 txbas 12338 blin2 12512 xmettxlem 12589 xmettx 12590 addcncntoplem 12631 mulcncf 12671 |
Copyright terms: Public domain | W3C validator |