7.2.3 Existential elimination

Extracting some truth from a $\exists xPx$ is tricky, but it's done this way:

$$\begin{fitch*} \par m & \exists x A \\ \par n & \fh A\{a/x\}... ... \par \hline \par & B & E$\exists$\ m,n,p,a \par \end{fitch*}$$

So, if one of the $A$ implies $B$, then we know that $B$, since we know that one of the $A$ is true. No $a$ should appear in $B$ nor in any attainable hypothesis (sorry for the cryptical phrases, they are part of the theory).