Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exlimdv | Unicode version |
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
exlimdv.1 |
Ref | Expression |
---|---|
exlimdv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1419 | . 2 | |
2 | ax-17 1419 | . 2 | |
3 | exlimdv.1 | . 2 | |
4 | 1, 2, 3 | exlimdh 1487 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-5 1336 ax-gen 1338 ax-ie2 1383 ax-17 1419 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ax11v2 1701 exlimdvv 1777 exlimddv 1778 tpid3g 3483 sssnm 3525 euotd 3991 ralxfr2d 4196 rexxfr2d 4197 releldmb 4571 relelrnb 4572 elres 4646 iss 4654 imain 4981 elunirn 5405 ovmpt4g 5623 op1steq 5805 fo2ndf 5848 reldmtpos 5868 rntpos 5872 tfrlemibacc 5940 tfrlemibxssdm 5941 tfrlemibfn 5942 tfrexlem 5948 freccl 5993 xpdom3m 6308 phplem4 6318 phpm 6327 findcard2 6346 findcard2s 6347 ac6sfi 6352 ordiso 6358 recclnq 6490 ltexnqq 6506 ltbtwnnqq 6513 recexprlemss1l 6733 recexprlemss1u 6734 negm 8550 climcau 9866 |
Copyright terms: Public domain | W3C validator |