![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exlimddv | GIF 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 1754 | . 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) |
5 | 1, 4 | mpd 13 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∃wex 1433 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ie2 1435 ax-17 1471 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: fvmptdv2 5428 tfrlemi14d 6136 tfrexlem 6137 tfr1onlemres 6152 tfrcllemres 6165 tfrcldm 6166 erref 6352 xpdom2 6627 dom0 6634 xpen 6641 mapdom1g 6643 phplem4dom 6658 phplem4on 6663 fidceq 6665 dif1en 6675 fin0 6681 fin0or 6682 isinfinf 6693 infm 6700 en2eqpr 6703 supelti 6777 djudom 6863 enomnilem 6881 exmidfodomrlemim 6924 genpml 7173 genpmu 7174 ltexprlemm 7256 ltexprlemfl 7265 ltexprlemfu 7267 eqord1 8058 nn1suc 8539 seq3f1oleml 10053 zfz1isolem1 10360 lmff 12100 exmidsbthrlem 12617 |
Copyright terms: Public domain | W3C validator |