First Order Logic (deduction proof in Hilbert system) 
Possible Duplicate:
First order logic proof question 

I need to prove this:
⊢ (∀x.ϕ) →(∃x.ϕ)
Using the following axioms:

The only thing I did was use deduction theorem:
(∀x.ϕ) ⊢(∃x.ϕ)
And then changed (∃x.ϕ) into (~∀x.~ϕ), so:
(∀x.ϕ) ⊢ (~∀x.~ϕ)
How can I continue with this? I cannot use soundness/completeness theorems.
EDIT: ∀* means it is a finite sequence of universal quantifiers (possible 0) 

If the asterisks in your axioms mean that the axioms are to be fully universally quantified, so that they become sentences, and if your language has no constant symbols, then it will not be possible to make the desired deduction in your system. The reason is that since all the axioms are fully universally quantified, they are (vacuously) true in the empty structure, and your rule of inference is truth-preserving for any structure including the empty structure. But your desired deduction is not valid for the empty structure, since the hypothesis is vacuously true there, but the conclusion is not. So it would actually be unsound for you to able to make that deduction. Your desired validity is only valid in nonempty domains, and so you need a formal system appropriate for reasoning in nonempty domains.
