diff --git a/library/standard/logic.lean b/library/standard/logic.lean
index 5f66206894..a3d0b9c26d 100644
--- a/library/standard/logic.lean
+++ b/library/standard/logic.lean
@@ -218,3 +218,6 @@ theorem inhabited_Bool [instance] : inhabited Bool
 
 theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
 := inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
+
+theorem inhabited_exists {A : Type} {P : A → Bool} (H : ∃ x, P x) : inhabited A
+:= obtain w Hw, from H, inhabited_intro w