Elimination of ∃ via ⊢

∃w_nphi, khi1, ... khik ⊢ psi if phi(a/w), khi1, ... khik ⊢ psi, provided

(1) that ∃w_nphi is the scope of ∃w_n

(2) that a does not occur in any of phi, khi1, ...,khik, psi.

-- and the caveat that substitutions are to preserve subscripts.

Grice, p. 127, in Davidson/Hintikka.