7.2.3 Eliminación del existencial

Sacar algo cierto de un $\exists xPx$ cuesta, pero se hace así:

$$\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*}$$

O sea, que si uno de los $A$ implica $B$, entonces sabemos que $B$, porque sabemos que uno de los $A$ es cierto. No debe aparecer ninguna $a$ en $B$ ni en ninguna hipótesis accesible (perdón por las frases crípticas; son parte de la teoría).