Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eximdv | Unicode version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 |
Ref | Expression |
---|---|
eximdv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1506 | . 2 | |
2 | alimdv.1 | . 2 | |
3 | 1, 2 | eximdh 1591 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1472 |
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 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2eximdv 1862 reximdv2 2556 cgsexg 2747 spc3egv 2804 euind 2899 ssel 3122 reupick 3391 reximdva0m 3409 uniss 3794 eusvnfb 4415 coss1 4742 coss2 4743 dmss 4786 dmcosseq 4858 funssres 5213 imain 5253 brprcneu 5462 fv3 5492 dffo4 5616 dffo5 5617 f1eqcocnv 5742 mapsn 6636 ctssdccl 7056 acfun 7143 ccfunen 7185 cc4f 7190 cc4n 7192 dmaddpq 7300 dmmulpq 7301 recexprlemlol 7547 recexprlemupu 7549 ioom 10164 ctinfom 12199 ctinf 12201 omctfn 12214 nninfdclemp1 12223 txcn 12717 |
Copyright terms: Public domain | W3C validator |