Let "provability formula" ${\rm Prf}(x, y)$ written in the manner that provability operator $\square A$ defined as $\exists x\ {\rm Prf}(x, \overline A)$ satisfying Hilbert–Bernays axioms:
If ZF $\vdash A$ then ZF $\vdash \square A$.
ZF $\vdash \square A \to \square \square A$.
ZF $\vdash (\square A \land \square (A \to B) \to \square B)$.
From here I have to prove Goedel's Theorem, i.e. ZF $\vdash (\square \neg \square \perp \to \square \perp)$. Here $\perp$ is some contradiction, for example $(\Phi \land \neg \Phi)$.
Usually implications can be derived using deduction lemma. But here I'm little bit confused. Or maybe I understand "prove" incorrectly, i.e. it is not derivation?
Assume that $T$ satisfies the Hilbert-Bernays conditions and that:
$T\vdash A \leftrightarrow (\Box A \to \bot)$
for some sentence $A$. Call this the diagonal sentence.
By the first and third conditions it follows that:
$T\vdash\Box A \to \Box(\Box A \to \bot)$
and thus by another application of the third condition:
$T\vdash\Box A \to (\Box\Box A \to \Box \bot)$
By the second condition we then get:
$T\vdash\Box A \to (\Box A \to \Box\bot)$
and thus:
$T\vdash\Box A \to \Box \bot$
Contraposition, the first and third condition then yield:
$T\vdash\Box\neg\Box\bot \to \Box\neg \Box A$
If we can show that $T\vdash\Box\neg\Box A \to \Box A$, then we'd be done. But the diagonal sentence can also be written:
$T\vdash A\leftrightarrow \neg\Box A$
Thus:
$T\vdash\neg \Box A \to A$
We can then apply the first and third conditions again to get $T\vdash\Box\neg\Box A \to \Box A$ as required.