Modus ponens proof in system L(¬,→,∙)

Question

I'm trying to prove $\neg\neg\bullet\varphi$

in system $L(\neg, \to, \bullet)$, where $\bullet$ is constant truth, i.e. $\bullet \varphi \approx (\varphi \to \varphi)$

Using modus ponens with axiomas:

A1) $\neg\neg\bullet\bullet\varphi$

A2) $(\neg\bullet\varphi \to \neg \psi)$

A3) $((\varphi\to\psi) \to (\neg\psi\to\neg\varphi))$

but still with no success. Could anybody suggest me some flow of proof?

Answer 1

Hint Take $\psi=\bullet\bullet\varphi$ in A2 and apply A3 and modus ponens.