![]() |
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 1526 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | alimdv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eximdh 1611 |
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-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 2eximdv 1882 reximdv2 2576 cgsexg 2772 spc3egv 2829 euind 2924 ssel 3149 reupick 3419 reximdva0m 3438 uniss 3830 eusvnfb 4453 coss1 4781 coss2 4782 dmss 4825 dmcosseq 4897 funssres 5257 imain 5297 brprcneu 5507 fv3 5537 dffo4 5663 dffo5 5664 f1eqcocnv 5789 mapsn 6687 ctssdccl 7107 acfun 7203 ccfunen 7260 cc4f 7265 cc4n 7267 dmaddpq 7375 dmmulpq 7376 recexprlemlol 7622 recexprlemupu 7624 ioom 10256 ctinfom 12421 ctinf 12423 omctfn 12436 nninfdclemp1 12443 subgintm 12989 txcn 13646 |
Copyright terms: Public domain | W3C validator |