![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eximii | GIF version |
Description: Inference associated with eximi 1580. (Contributed by BJ, 3-Feb-2018.) |
Ref | Expression |
---|---|
eximii.1 | ⊢ ∃𝑥𝜑 |
eximii.2 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
eximii | ⊢ ∃𝑥𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximii.1 | . 2 ⊢ ∃𝑥𝜑 | |
2 | eximii.2 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 2 | eximi 1580 | . 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ∃𝑥𝜓 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1469 |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-ial 1515 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax6evr 1682 spimed 1719 darii 2100 barbari 2102 festino 2106 baroco 2107 cesaro 2108 camestros 2109 datisi 2110 disamis 2111 felapton 2114 darapti 2115 dimatis 2117 fresison 2118 calemos 2119 fesapo 2120 bamalip 2121 vtoclf 2742 vtocl2 2744 vtocl3 2745 nalset 4066 el 4110 dtruarb 4123 snnex 4377 eusv2nf 4385 dtruex 4482 limom 4535 bj-axemptylem 13261 bj-nalset 13264 bj-d0clsepcl 13294 bj-omex2 13346 bj-nn0sucALT 13347 |
Copyright terms: Public domain | W3C validator |