Inference rule: Existential elimination/instantiation (declared)

Suppose that x and y are variables such that y does not occur in either of the statements \phi or \psi , nor in any assumption in the current context. Given that the existence statement \exists x \phi holds and the variable substitution [\phi | x \to y] entails \psi , we may that infer that \psi holds: \cfrac{\vdash \exists x \phi \quad [\phi | x \to y] \vdash \psi}{\vdash \psi}.