Proving that this statement is a theorem of our proof system

Question

So I need to produce a proof tree of the below statement using the introduction and elimination rules.

$$ \begin{array}{c} x \in a &q \\ \hline \exists x \colon a \bullet q \\ \hline ((\exists x \colon a \bullet p) \land (\forall x \colon a \bullet p \implies q)) \implies (\exists x \colon a \bullet q) \end{array} $$

I know I'll have to do an exists introduction as the next step but am I on the right track? The example I have does two trees, one for the right side and one for the left. I'm confused about where I need to go with this.

Answer 1

I assume $p$ and $q$ may contain instances of $x$? If so, I really prefer to work with $\exists x \ p(x)$ rather than $\forall x \ p$. Also, I'll leave out the $x \in a$ part ... you can add it back in if you want, but here is the basic proof:

\begin{align} \cfrac{\cfrac{\cfrac{\cfrac{\exists x \ p(x) \land \forall x (p(x) \to q(x))^1}{\cfrac{\exists x \ p(x)}{p(a)}{\ \exists E} \qquad \cfrac{\forall x (p(x) \to q(x))}{p(a) \to q(a)}{\ \forall E}}{\ \land E}}{q(a)}{\ \to E}}{\exists x \ q(x)}{\ \exists I}}{(\exists x \ P(x)) \land \forall x (p(x) \to q(x))) \to \exists x \ q(x)}{\ \to I^1} \end{align}

The subscript $1$ shows which statement is being discharged at which point in the proof.