Prove a predicate formula in the constructive logic

Question

Using the constructive logic (the axiom $A\lor\lnot A$ cannot be used), using quantifier axioms and Modus Ponens, and Generalization, prove the following:

$\exists x(B(x) \to C(x)) \to (\forall xB(x) \to \exists x C(x))$

Taking as hypotheses:

$\exists x(B(x) \to C(x))$ ;

$\forall xB(x)$ ;

We now need to show that

$ \exists x C(x) $

and then by Deduction theorem 2 we will be able to say that there is a proof of the initial formula.

I can get only so far that I get $B(x)$ and then I'm stuck. How should I approach this?

Note that $B \to C$ cannot be substituted by $\lnot B\lor C$

Answer 1

Start from $\exists x(B(x) \to C(x))$ and use existential instantiation with the new introduced constant (variable) $a$ to get $B(a) \to C(a).$ Now apply $\forall x B(x)$ by universal instantiation to get $B(a).$ At this point from modus ponens and the two already shown $B(a)$ and $B(a) \to C(a),$ we get to $C(a),$ and then using existential generalization finally arrive at $\exists x C(x).$

Note: I assume your system must have versions of universal/existential instantiation and existential generalization. Without something like that I don't see how to prove it either.