We cannot prove it ...
As said in your previous post :
in system $\mathcal L(\neg, \to, \bullet)$, $\bullet$ "acts" as a constant truth, i.e. $\bullet \varphi \approx (\varphi \to \varphi)$.
If we consider the usual truth functional properties of the conncetives : $\lnot, \rightarrow$, and replace $\bullet \varphi$ with $\top$ ("the true"), we have that :
A1) $\neg\neg\bullet\bullet\varphi$ is $\neg \neg (\top \to \top)$, that is always $\top$
A2) $(\neg\bullet\varphi \to \neg \psi)$ is $(\neg \top \to \neg \psi)$, that is $(\bot \to \neg \psi)$, and again it is always $\top$
A3) $((\varphi\to\psi) \to (\neg\psi\to\neg\varphi))$ is a tautology; thus it is also $\top$.
Of course, modus ponens preserves validity.
$\neg\bullet\varphi$ is $\neg \top$ i.e. $\bot$.