7.2.3 Eliminació de l'existencial

Treure quelcom cert d'un $\exists xPx$ costa, però es fa així:

$$\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 sigui, que si un dels $A$ implica $B$, llavors sabem que $B$, perquè sabem que un dels $A$ és cert. No ha d'aparèixer cap $a$ en $B$ ni en cap hipòtesi accesible (perdó per les frases críptiques; són part de la teoria).