![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exlimddv | Unicode version |
Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.) |
Ref | Expression |
---|---|
exlimddv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
exlimddv.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exlimddv |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimddv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | exlimddv.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | ex 115 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | exlimdv 1819 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpd 13 |
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-ia3 108 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: fvmptdv2 5605 tfrlemi14d 6333 tfrexlem 6334 tfr1onlemres 6349 tfrcllemres 6362 tfrcldm 6363 erref 6554 xpdom2 6830 dom0 6837 xpen 6844 mapdom1g 6846 phplem4dom 6861 phplem4on 6866 fidceq 6868 dif1en 6878 fin0 6884 fin0or 6885 isinfinf 6896 infm 6903 en2eqpr 6906 fiuni 6976 supelti 7000 djudom 7091 difinfsn 7098 enomnilem 7135 enmkvlem 7158 enwomnilem 7166 exmidfodomrlemim 7199 exmidaclem 7206 cc2lem 7264 cc3 7266 genpml 7515 genpmu 7516 ltexprlemm 7598 ltexprlemfl 7607 ltexprlemfu 7609 suplocsr 7807 axpre-suploc 7900 eqord1 8439 nn1suc 8937 seq3f1oleml 10502 zfz1isolem1 10819 nninfdcex 11953 zsupssdc 11954 eulerth 12232 ennnfonelemim 12424 exmidunben 12426 enctlem 12432 ctiunct 12440 unct 12442 omctfn 12443 omiunct 12444 issubg2m 13047 lmff 13685 txcn 13711 suplociccreex 14038 suplociccex 14039 subctctexmid 14686 exmidsbthrlem 14706 sbthom 14710 |
Copyright terms: Public domain | W3C validator |