Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eximii | GIF version |
Description: Inference associated with eximi 1588. (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 1588 | . 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ∃𝑥𝜓 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1480 |
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 1435 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-4 1498 ax-ial 1522 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: spimfv 1687 ax6evr 1693 spimed 1728 darii 2114 barbari 2116 festino 2120 baroco 2121 cesaro 2122 camestros 2123 datisi 2124 disamis 2125 felapton 2128 darapti 2129 dimatis 2131 fresison 2132 calemos 2133 fesapo 2134 bamalip 2135 vtoclf 2779 vtocl2 2781 vtocl3 2782 nalset 4112 el 4157 dtruarb 4170 snnex 4426 eusv2nf 4434 dtruex 4536 limom 4591 bj-axemptylem 13774 bj-nalset 13777 bj-d0clsepcl 13807 bj-omex2 13859 bj-nn0sucALT 13860 |
Copyright terms: Public domain | W3C validator |