![]() |
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 1526 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-17 1526 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | exlimdv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | exlimdh 1596 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-5 1447 ax-gen 1449 ax-ie2 1494 ax-17 1526 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ax11v2 1820 exlimdvv 1897 exlimddv 1898 tpid3g 3707 sssnm 3754 pwntru 4199 euotd 4254 ralxfr2d 4464 rexxfr2d 4465 releldmb 4864 relelrnb 4865 elres 4943 iss 4953 imain 5298 elunirn 5766 ovmpt4g 5996 oprssdmm 6171 op1steq 6179 fo2ndf 6227 reldmtpos 6253 rntpos 6257 tfrlemibacc 6326 tfrlemibxssdm 6327 tfrlemibfn 6328 tfrexlem 6334 tfr1onlembacc 6342 tfr1onlembxssdm 6343 tfr1onlembfn 6344 tfrcllembacc 6355 tfrcllembxssdm 6356 tfrcllembfn 6357 map0g 6687 xpdom3m 6833 phplem4 6854 phpm 6864 findcard2 6888 findcard2s 6889 ac6sfi 6897 fiintim 6927 xpfi 6928 fidcenum 6954 ordiso 7034 ctmlemr 7106 ctm 7107 ctssdc 7111 pm54.43 7188 exmidfodomrlemim 7199 recclnq 7390 ltexnqq 7406 ltbtwnnqq 7413 recexprlemss1l 7633 recexprlemss1u 7634 negm 9613 ioom 10258 seq3f1olemp 10499 fiinfnf1o 10761 fihashf1rn 10763 climcau 11350 summodclem2 11385 zsumdc 11387 isumz 11392 fsumf1o 11393 fisumss 11395 fsumcl2lem 11401 fsumadd 11409 fsummulc2 11451 ntrivcvgap 11551 prodmodclem2 11580 zproddc 11582 prod1dc 11589 fprodf1o 11591 fprodssdc 11593 fprodmul 11594 nnmindc 12029 uzwodc 12032 pceu 12289 ennnfone 12420 enctlem 12427 unct 12437 sgrpidmndm 12775 subrgintm 13324 eltg3 13450 tgtop 13461 tgidm 13467 tgrest 13562 tgcn 13601 xblm 13810 dvfgg 14050 dvcnp2cntop 14056 pwtrufal 14629 |
Copyright terms: Public domain | W3C validator |