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 114 | . . 3 |
4 | 3 | exlimdv 1775 | . 2 |
5 | 1, 4 | mpd 13 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wex 1453 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ie2 1455 ax-17 1491 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: fvmptdv2 5478 tfrlemi14d 6198 tfrexlem 6199 tfr1onlemres 6214 tfrcllemres 6227 tfrcldm 6228 erref 6417 xpdom2 6693 dom0 6700 xpen 6707 mapdom1g 6709 phplem4dom 6724 phplem4on 6729 fidceq 6731 dif1en 6741 fin0 6747 fin0or 6748 isinfinf 6759 infm 6766 en2eqpr 6769 fiuni 6834 supelti 6857 djudom 6946 difinfsn 6953 enomnilem 6978 exmidfodomrlemim 7025 exmidaclem 7032 genpml 7293 genpmu 7294 ltexprlemm 7376 ltexprlemfl 7385 ltexprlemfu 7387 suplocsr 7585 axpre-suploc 7678 eqord1 8213 nn1suc 8703 seq3f1oleml 10231 zfz1isolem1 10538 ennnfonelemim 11848 exmidunben 11850 enctlem 11856 ctiunct 11864 unct 11865 lmff 12329 txcn 12355 suplociccreex 12682 suplociccex 12683 subctctexmid 13092 exmidsbthrlem 13113 sbthom 13117 |
Copyright terms: Public domain | W3C validator |