Proving a bi-conditional predicate calculus formulae Prove the following:
∀x(C → D(x)) ↔ (C →∀xD(x))

I am looking at the axioms I can use under hilberts deductive system as well as the Generalization rule but I can't find an axiom that supports the biconditional connective. any help?
 A: We have to prove that, if $x$ does not occur free in $C$, then

$\vdash (C → ∀xD(x)) ↔ ∀x(C → D(x))$.



A) To prove :

$\vdash (C → ∀xD(x)) → ∀x(C → D(x))$.

1) $C → ∀xD(x)$ --- assumed
2) $C$ --- assumed
3) $∀xD(x)$ --- from 1) and 2) by modus ponens
4) $D(x)$ --- from 3) and Axiom.1 : $∀x \alpha → \alpha _t^x$, by mp
5) $C → D(x)$ --- from 2) and 4) by Deduction Th
6) $∀x(C → D(x))$ --- from 5) by Generalization Th : $x$ is not free in assumption 1)

7) $(C → ∀xD(x)) \rightarrow ∀x(C → D(x))$ --- from 1) and 6) by Deduction Th


B) To prove :

$\vdash ∀x(C → D(x)) → (C → ∀xD(x))$.

1) $∀x(C → D(x))$ --- assumed
2) $C$ --- assumed
3) $C → D(x)$ --- from 1) and Axiom.1 by mp
4) $D(x)$ --- from 2) and 3) by mp
5) $∀x D(x)$ --- from 4)  by Generalization Th : $x$ is not free in assumptions 1) and 2)
6)  $C → ∀x D(x)$ --- from 2) and 5) by Deduction Th

7) $∀x(C → D(x)) → (C → ∀x D(x))$ --- from 1) and 6) by Deduction Th


The theorem follows from A) and B) by tautological implication :


$\alpha \rightarrow \beta, \beta \rightarrow \alpha \vDash \alpha \leftrightarrow \beta$


