![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eximii | GIF version |
Description: Inference associated with eximi 1600. (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 1600 | . 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ∃𝑥𝜓 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: spimfv 1699 ax6evr 1705 spimed 1740 darii 2126 barbari 2128 festino 2132 baroco 2133 cesaro 2134 camestros 2135 datisi 2136 disamis 2137 felapton 2140 darapti 2141 dimatis 2143 fresison 2144 calemos 2145 fesapo 2146 bamalip 2147 vtoclf 2790 vtocl2 2792 vtocl3 2793 nalset 4132 el 4177 dtruarb 4190 snnex 4447 eusv2nf 4455 dtruex 4557 limom 4612 bj-axemptylem 14504 bj-nalset 14507 bj-d0clsepcl 14537 bj-omex2 14589 bj-nn0sucALT 14590 |
Copyright terms: Public domain | W3C validator |