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 1459 | . 2 | |
2 | ax-17 1459 | . 2 | |
3 | exlimdv.1 | . 2 | |
4 | 1, 2, 3 | exlimdh 1527 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1421 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-5 1376 ax-gen 1378 ax-ie2 1423 ax-17 1459 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: ax11v2 1741 exlimdvv 1818 exlimddv 1819 tpid3g 3505 sssnm 3546 euotd 4009 ralxfr2d 4214 rexxfr2d 4215 releldmb 4589 relelrnb 4590 elres 4664 iss 4674 imain 5001 elunirn 5426 ovmpt4g 5643 op1steq 5825 fo2ndf 5868 reldmtpos 5891 rntpos 5895 tfrlemibacc 5963 tfrlemibxssdm 5964 tfrlemibfn 5965 tfrexlem 5971 freccl 6016 xpdom3m 6331 phplem4 6341 phpm 6351 findcard2 6373 findcard2s 6374 ac6sfi 6379 ordiso 6447 pm54.43 6459 recclnq 6582 ltexnqq 6598 ltbtwnnqq 6605 recexprlemss1l 6825 recexprlemss1u 6826 negm 8700 ioom 9269 climcau 10184 |
Copyright terms: Public domain | W3C validator |