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 1590 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1468 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2eximdv 1854 reximdv2 2529 cgsexg 2716 spc3egv 2772 euind 2866 ssel 3086 reupick 3355 reximdva0m 3373 uniss 3752 eusvnfb 4370 coss1 4689 coss2 4690 dmss 4733 dmcosseq 4805 funssres 5160 imain 5200 brprcneu 5407 fv3 5437 dffo4 5561 dffo5 5562 f1eqcocnv 5685 mapsn 6577 ctssdccl 6989 acfun 7056 ccfunen 7072 dmaddpq 7180 dmmulpq 7181 recexprlemlol 7427 recexprlemupu 7429 ioom 10031 ctinfom 11930 ctinf 11932 txcn 12433 |
Copyright terms: Public domain | W3C validator |