How to derive the following theorem? 
How to prove this
$$\vdash\forall x (B\land C)\leftrightarrow(\forall x B\land\forall x C)$$?

Here is my failed attempt:(
First I have two options to prove it:

*

*To suppose $\vdash\forall x (B\land C)$ and to prove $(\forall x B\land\forall x C)$ and then to do the converse.

OR


*$\vdash[\forall x (B\land C)\to(\forall x B\land\forall x C)]\land [\forall x (B\land C)\leftrightarrow(\forall x B\land\forall x C)]$
But in 2. I won't be able to use the Deduction Theorem. So I chose 1.
And I also tried to do an analogy of the proof of this theorem $$\vdash\forall x(B\to C)\to(\forall x B\to\forall x C)...(*)$$
I tried to change the $\land$ by $\to$ to make the theorem look like (*):
By hypothesis $\vdash\forall x (B\land C)$, but it's equivalent to
$\forall x\lnot(B\to\lnot C)$. By A4, $\lnot(B\to\lnot C)$ and here a problem appears since I won't be able to apply modus ponens to obtain $C$ or $\lnot C$ like it was done in the proof of (*).
Note: I can only use the axioms, modus ponens and the Gen rule.


 A: As correctly remarked by Bram28, $\mathscr{A} \land \mathscr{B}$ is nothing but  a shorthand for $\lnot (\mathscr{A} \to \lnot \mathscr{B})$, since in your system $\mathsf{K}$ there are no axioms dealing with $\land$. Similarly for $\mathscr{A} \leftrightarrow \mathscr{B}$, seen as a shorthand for $(\mathscr{A} \to \mathscr{B}) \land (\mathscr{B} \to \mathscr{A})$.
This means that you have to prove 
$$\lnot \big( (\forall x\lnot(B\to \lnot C)\to\lnot(\forall x B\to\lnot\forall xC)) \to \lnot(\lnot(\forall xB\to\lnot\forall x C)\to\forall x\lnot(B\to\lnot C)) \big)$$ 
in your system $\mathsf{K}$. Finding a direct derivation of such a formula seems to be a very hard task, and the derivation could be huge and unintelligible.
An alternative, but equivalent, approach is to take seriously the idea of $\mathscr{A} \land \mathscr{B}$ as a shorthand for $\lnot (\mathscr{A} \to \lnot \mathscr{B})$ and to reason about $\mathscr{A} \land \mathscr{B}$ (which is easier to handle) instead of $\lnot (\mathscr{A} \to \lnot \mathscr{B})$. Of course, in order to be entitled to do this, we first have to prove in the system $\mathsf{K}$ that $\mathscr{A} \land \mathscr{B}$ (i.e. $\lnot (\mathscr{A} \to \lnot \mathscr{B})$) fulfills some natural introduction and elimination rules; in other words, we have to prove that the following formulas are derivable in the system $\mathsf{K}$:
\begin{align*}
(\land_\text{intro})\quad& \mathscr{A} \to (\mathscr{B} \to (\mathscr{A} \land \mathscr{B})) &\text{i.e.}\quad & \mathscr{A} \to (\mathscr{B} \to \lnot(\mathscr{A} \to \lnot \mathscr{B})) \\
(\land_\text{elim1})\quad& (\mathscr{A} \land \mathscr{B}) \to \mathscr{A} &\text{i.e.}\quad & \lnot(\mathscr{A} \to \lnot \mathscr{B}) \to \mathscr{A} \\
(\land_\text{elim2})\quad& (\mathscr{A} \land \mathscr{B}) \to \mathscr{B} &\text{i.e.}\quad & \lnot(\mathscr{A} \to \lnot \mathscr{B}) \to \mathscr{B} 
\end{align*}


*

*Proof that $\land_\text{intro}$ is derivable in $\mathsf{K}$. First, as a preliminary step, the derivation below shows that $\lnot \lnot (\mathscr{A} \to \lnot \mathscr{B}), \, \mathscr{A} \vdash_\mathsf{K} \lnot \mathscr{B}$.  Let $\mathscr{C} = \mathscr{A} \to \lnot \mathscr{B}$:
\begin{align}
1. \ &(\lnot\mathscr{C} \to \lnot\lnot\mathscr{C}) \to ((\lnot\mathscr{C} \to \lnot\mathscr{C}) \to \mathscr{C}) &\text{(by axiom $A_3$)} \\
2. \ &\lnot\lnot\mathscr{C} \to (\lnot \mathscr{C} \to \lnot\lnot \mathscr{C}) &\text{(by axiom $A_1$)} \\
3. \ &\lnot\lnot\mathscr{C} &\text{(by hypothesis)} \\
4. \ &\lnot \mathscr{C} \to \lnot\lnot\mathscr{C} &\text{(by $\mathsf{MP}$ with 2 and 3)} \\
5. \ &(\lnot\mathscr{C} \to \lnot\mathscr{C}) \to \mathscr{C} &\text{(by $\mathsf{MP}$ with 1 and 4)} \\
6. \ &\big(\lnot\mathscr{C} \to ((\lnot\mathscr{C} \to \lnot\mathscr{C}) \to \lnot\mathscr{C}) \big) \to \big( (\lnot\mathscr{C} \to (\lnot\mathscr{C} \to \lnot\mathscr{C})) \to (\lnot\mathscr{C} \to \lnot\mathscr{C}) \big) &\text{(by axiom $A_2$)} \\
7. \ &\lnot\mathscr{C} \to ((\lnot\mathscr{C} \to \lnot\mathscr{C}) \to \lnot\mathscr{C}) &\text{(by axiom $A_1$)} \\
8. \ &(\lnot\mathscr{C} \to (\lnot\mathscr{C} \to \lnot\mathscr{C})) \to (\lnot\mathscr{C} \to \lnot\mathscr{C}) &\text{(by $\mathsf{MP}$ with 6 and 7)} \\
9. \ &\lnot\mathscr{C} \to (\lnot\mathscr{C} \to \lnot\mathscr{C}) &\text{(by axiom $A_1$)} \\
10. \ &\lnot\mathscr{C} \to \lnot\mathscr{C} &\text{(by $\mathsf{MP}$ with 8 and 9)} \\
11. \ &\mathscr{A} \to \lnot \mathscr{B} &\text{(by $\mathsf{MP}$ with 5 and 10)} \\
12. \ &\mathscr{A} &\text{(by hypothesis)} \\
13. \ &\lnot\mathscr{B} &\text{(by $\mathsf{MP}$ with 11 and 12)}
\end{align}
From the Deduction Theorem, it follows that $\mathscr{A} \vdash_\mathsf{K} \lnot\lnot (\mathscr{A} \to \lnot \mathscr{B}) \to \lnot \mathscr{B}$ [$*$].
Now we can use $[*]$ in the derivation below to prove that $\mathscr{A}, \,\mathscr{B} \vdash_\mathsf{K} \lnot(\mathscr{A} \to \lnot \mathscr{B})$. Recall that $\mathscr{C} = \mathscr{A} \to \lnot \mathscr{B}$.
\begin{align}
1. \ &(\lnot\lnot\mathscr{C} \to \lnot \mathscr{B}) \to ((\lnot\lnot\mathscr{C} \to \mathscr{B}) \to \lnot \mathscr{C}) &\text{(by axiom $A_3$)} \\
2. \ &\mathscr{A} &\text{(by hypothesis)} \\
3. \ &\lnot\lnot \mathscr{C} \to \lnot \mathscr{B} &\text{(by $[*]$, from 2)} \\
4. \ &(\lnot\lnot\mathscr{C} \to \mathscr{B}) \to \lnot \mathscr{C} &\text{(by $\mathsf{MP}$ with 1 and 3)} \\
5. \ &\mathscr{B} \to (\lnot\lnot\mathscr{C} \to \mathscr{B}) &\text{(by axiom $A_1$)} \\
6. \ &\mathscr{B} &\text{(by hypothesis)} \\
7. \ &\lnot\lnot\mathscr{C} \to \mathscr{B}  &\text{(by $\mathsf{MP}$ with 5 and 6)} \\
8. \ &\lnot(\mathscr{A} \to \lnot\mathscr{B}) &\text{(by $\mathsf{MP}$ with 4 and 7)}
\end{align}
From the Deduction Theorem (applied twice), it follows that $\vdash_\mathsf{K} \mathscr{A} \to (\mathscr{B} \to \lnot (\mathscr{A} \to \lnot \mathscr{B}))$.

*Proof that $\land_\text{elim1}$ is derivable in $\mathsf{K}$: similar to the point below, slightly more complicated. A good exercise for the reader.

*Proof that $\land_\text{elim2}$ is derivable in $\mathsf{K}$. The derivation below shows that $\lnot(\mathscr{A} \to \lnot \mathscr{B}) \vdash_\mathsf{K} \mathscr{B}$. 
\begin{align}
1. \ &(\lnot\mathscr{B} \to \lnot(\mathscr{A} \to \lnot \mathscr{B})) \to \big((\lnot\mathscr{B} \to (\mathscr{A} \to \lnot \mathscr{B})) \to \mathscr{B}\big) &\text{(by axiom $A_3$)} \\
2. \ &\lnot(\mathscr{A} \to \lnot \mathscr{B}) \to \big(\lnot \mathscr{B} \to \lnot (\mathscr{A} \to \lnot \mathscr{B}) \big) &\text{(by axiom $A_1$)} \\
3. \ &\lnot(\mathscr{A} \to \lnot \mathscr{B}) &\text{(by hypothesis)} \\
4. \ &\lnot \mathscr{B} \to \lnot (\mathscr{A} \to \lnot \mathscr{B}) &\text{(by $\mathsf{MP}$ with $2$ and $3$)} \\
5. \ &(\lnot\mathscr{B} \to (\mathscr{A} \to \lnot \mathscr{B})) \to \mathscr{B} &\text{(by $\mathsf{MP}$ with $1$ and $4$)} \\
6. \ &\lnot\mathscr{B} \to (\mathscr{A} \to \lnot \mathscr{B}) &\text{(by axiom $A_1$)} \\
7. \ &\mathscr{B} &\text{(by $\mathsf{MP}$ with $1$ and $5$)}
\end{align}
From the Deduction Theorem, it follows that $\vdash_\mathsf{K} \lnot(\mathscr{A} \to \lnot \mathscr{B}) \to \mathscr{B}$.
The advantage of proving $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$ is that $\mathscr{A} \land \mathscr{B}$ is still nothing but $\lnot (\mathscr{A} \to \lnot \mathscr{B})$, but now when dealing with $\mathscr{A} \land \mathscr{B}$ you can directly use $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$ and "forget" about its syntactic definition as $\lnot (\mathscr{A} \to \lnot \mathscr{B})$: this definition  still holds but is "hidden" in the derivations of $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$.
Using $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$, we can prove that $\forall x (B \land C) \vdash_\mathsf{K} \forall x B \land \forall x C$, i.e. $\forall x \, \lnot(B \to \lnot C) \vdash_\mathsf{K} \lnot(\forall x B \to \lnot \forall x C)$, as shown by the derivation below.
\begin{align}
1. \ &\forall x (B \land C) \to (B \land C) &\text{(by axiom $A_4$)} \\
2. \ &\forall x B \to (\forall x C \to (\forall x B \land \forall x C)) &\text{(by $\land_\text{intro}$)} \\
3. \ &(B \land C) \to B &\text{(by $\land_\text{elim1}$)} \\
4. \ &(B \land C) \to C &\text{(by $\land_\text{elim2}$)} \\
5. \ &\forall x (B \land C) &\text{(by hypothesis)} \\
6. \ &B \land C &\text{(by $\mathsf{MP}$ with 1 and 5)} \\
7. \ &B &\text{(by $\mathsf{MP}$ with 3 and 6)} \\
8. \ &\forall x B &\text{(by generalization of 7)} \\
9. \ &\forall x C \to (\forall x B \land \forall x C) &\text{(by $\mathsf{MP}$ with 2 and 8)} \\
10. \ &C &\text{(by $\mathsf{MP}$ with 4 and 6)} \\
11. \ &\forall x C &\text{(by generalization of 10)} \\
12. \ &\forall x B \land \forall x C &\text{(by $\mathsf{MP}$ with 9 and 11)}
\end{align}
From the Deduction Theorem, it follows that $\vdash_\mathsf{K} \forall x (B \land C) \to (\forall x B \land \forall x C)$ $[**]$.
Using $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$, we can prove that $\forall x (B \land C) \vdash_\mathsf{K} \forall x B \land \forall x C$, i.e. $\forall x \, \lnot(B \to \lnot C) \vdash_\mathsf{K} \lnot(\forall x B \to \lnot \forall x C)$, as shown by the derivation below.
\begin{align}
1. \ &(\forall x B \land \forall x C) \to \forall x B &\text{(by $\land_\text{elim1}$)} \\
2. \ &(\forall x B \land \forall x C) \to \forall x C &\text{(by $\land_\text{elim2}$)} \\
3. \ &B \to (C \to (B \land C)) &\text{(by $\land_\text{intro}$)} \\
4. \ &\forall x B \land \forall x C &\text{(by hypothesis)} \\
5. \ &\forall x B &\text{(by $\mathsf{MP}$ with 1 and 4)} \\
6. \ &\forall x C &\text{(by $\mathsf{MP}$ with 2 and 4)} \\
7. \ &\forall x B \to B &\text{(by axiom $A_4$)} \\
8. \ &\forall x C \to C &\text{(by axiom $A_4$)} \\
9. \ &B &\text{(by $\mathsf{MP}$ with 7 and 5)} \\
10. \ &C &\text{(by $\mathsf{MP}$ with 8 and 6)} \\
11. \ &C \to (B \land C) &\text{(by $\mathsf{MP}$ with 3 and 9)} \\
12. \ &B \land C &\text{(by $\mathsf{MP}$ with 11 and 10)} \\
13. \ &\forall x (B \land C) &\text{(by generalization of 12)}
\end{align}
From the Deduction Theorem, it follows that $\vdash_\mathsf{K} (\forall x B \land \forall x C) \to \forall x (B \land C)$ $[***]$.
Finally, using $[**]$, $[***]$ and $\land_\text{intro}$, we can prove that $\vdash_\mathsf{K} \big(∀x(B∧C)→(∀xB∧∀xC) \big) \land \big( (∀xB ∧ ∀xC) \to ∀x(B∧C) \big)$, i.e. $\vdash_\mathsf{K} (∀x(B∧C)↔(∀xB∧∀xC))$, as shown by the following derivation. Let $\mathscr{C} = ∀x(B∧C)→(∀xB∧∀xC)$ and $\mathscr{D} = (∀xB ∧ ∀xC) \to ∀x(B∧C)$.
\begin{align}
1. \ &\mathscr{C} \to (\mathscr{D} \to (\mathscr{C} \land \mathscr{D})) &\text{(by $\land_\text{intro}$)} \\
2. \ &\mathscr{C} &\text{(by $[**]$)} \\
3. \ &\mathscr{D} \to (\mathscr{C} \land \mathscr{D}) &\text{(by $\mathsf{MP}$ with 1 and 2)} \\
4. \ &\mathscr{D} &\text{(by $[***]$)} \\
5. \ &\mathscr{C} \land \mathscr{D} &\text{(by $\mathsf{MP}$ with 3 and 4)}
\end{align}
