how can i use the deduction theorem to show a basic property? i'm wondering - how can i use the deduction property to show those two:
1)$\vdash \forall x (p(x) \to q(x)) \to (\exists x p(x) \to \exists x q(x))$
2)$\vdash \forall x (p(x) \to q(x)) \to (\forall x p(x) \to \forall x q(x))$
if there's a better way to prove it (formal proof), i would be interested in learning how to do so.
it seems quite trivial to understand that if $\vdash \forall x (p(x) \to q(x)$ then must exists an x that follows it ($(∃xp(x)→∃xq(x))$ or to put the $\forall$ inside the brackets.
however, i don't know how to prove it and would really appreciate learning how to do so correctly, even though it might seem trivial.
thank you very much for your help
my attempt with 1) after the given answer for 2):
1) $∀x(p(x)→q(x))$ --- assumed
2) $\exists p(x)$ --- assumed
3)$p(c)$
3) $⊢∀x(p(x)→q(x))$ --- 
4) $⊢∀x(p(x)→q(x))→(p(c)→q(c))$ --- quantifier axiom, assumption
5) $p(C)→q(C)$ --- assignment
6) q(c) --- from 2) and 5) by Modus Ponens
7) $\exists x p(c)$ --- 
8) $\exists x q(c)$ --- 
9) $\exists xp(x)→\exists xq(x)$ --- from 2) and 8) by Deduction Theorem
10) $⊢∀x(p(x)→q(x))→(\exists xp(x)→\exists xq(x))$ --- from 1) and 9) by Deduction Theorem
 A: Consider 2) :
1) $∀x(p(x) → q(x))$ --- assumed 
2) $∀xp(x)$ --- assumed
3) $\vdash ∀x(p(x) → q(x)) \to (p(x) → q(x))$ --- quantifier axiom
4) $p(x) → q(x)$ --- from 1) and 3) by Modus Ponens
5) $\vdash ∀xp(x) \to p(x)$ --- quantifier axiom
6) $p(x)$ --- from 2) and 5) by Modus Ponens
7) $q(x)$ --- from 4) and 6) by Modus Ponens
8) $∀xq(x)$ --- from 7) by Generalization
9) $∀xp(x) \to ∀xq(x)$ --- from 2) and 8) by Deduction Theorem

10) $\vdash ∀x(p(x) → q(x)) \to (∀xp(x) \to ∀xq(x))$ --- from 1) and 9) by Deduction Theorem


For axioms and rules, see E.Mendelson, Introduction to Mathematical Logic, Ch,2 First-Order Logic.

We can prove 1) with Hilbert-calculus using the equivalence :

$¬∀¬ ≡ ∃$. 

From $∀x(p(x)→q(x))$ we derive $p(x)→q(x)$ and then $¬q(x)→¬p(x)$. 
Then we have to use Generalization and then apply 2) to get $∀x¬q(x) → ∀x¬p(x)$.
Finally, we use again contraposition to get : 

$¬∀x¬p(x) → ¬∀x¬q(x)$.

A: It's good to see your attempt at (1). Here is the proof in Fitch-style natural deduction:

If $\forall x( p(x) \to q(x) )$:
  If $\exists x( p(x) )$:
    Let $c$ be such that $p(c)$.   [$\exists$-elim]
    $p(c) \to q(c)$.   [$\forall$-elim]
    $q(c)$.   [$\to$-elim]
    $\exists x( q(x) )$.   [$\exists$-intro]
  $\exists x( p(x) ) \to \exists x( q(x) )$.   [$\to$-intro]
$\forall x( p(x) \to q(x) ) \to ( \exists x( p(x) ) \to \exists x( q(x) ) )$.   [$\to$-intro]

As you can see, it is supposed to directly reflect natural reasoning. In general, as DanielV said in a comment, Hilbert-style systems cannot be used by humans for practical mathematical work. In contrast, Fitch-style systems like the one I just used can be used in practice even for highly complex theorems and proofs. An additional bonus is that they are readily understood by any professional mathematician even if they have never seen the system before.
