How to syntactically prove $\emptyset \vdash \top$?

Question

$\emptyset \vdash \top$

I was trying to prove this using the Hilbert proof system and this is what I got:

(1)$ \top \equiv (\bot \equiv \bot)$ Axiom:$\top$ vs. $\bot$

(2)$ (\top \equiv \top)\equiv (\top \equiv (\bot \equiv \bot))$ by Leibniz

(3) $(\top \equiv \top)$ by equanimity on (2) and (1)

So this is where I am stuck. I confused on how I could use some axiom to isolate $\top$. Any help is much appreciated thank you! In my text-book if our assumptions are the $\emptyset$ then we can assume $\top$ is an absolute theorem but I am not sure how to go about proving this.

Axiom List: (https://i.sstatic.net/SjSH1.jpg)

Axioms of Boolean Logic $$\begin{array} \\ \text{ Associativity of } \equiv & ((A \equiv B) \equiv C) \equiv(A \equiv(B \equiv C)) \\ \text { Symmetry of } \equiv & (A \equiv B) \equiv(B \equiv A) \\ \text { Tvs. } \perp & T \equiv \perp \equiv \perp \\ \text { introduction of } \neg & \neg A \equiv A \equiv \perp \\ \text { Associativity of } \vee & (A \vee B) \vee C \equiv A\vee (B\vee C) \\ \text { Symmetry of } \vee & A \vee B \equiv B \vee A \\ \text { Idempotency of } \vee & A \vee A \equiv A \\ \text {Distributivity of } \vee \text{ over } \equiv & A \vee(B \equiv C) \equiv A \vee B \equiv A \vee C \\ \text { Excluded Middle } & A \vee \neg A \\ \text { Golden Rule } & A \wedge B \equiv A \equiv B \equiv A \vee B \\ \text { Implication } & A \rightarrow B \equiv A \vee B \equiv B \end{array} $$ Primary Rules of Inference $$\frac{A, A \equiv B}{B}\\~\\ \frac{A}{C[\mathbf{p}:=A] \equiv C[\mathbf{p}:=B]}$$

Book used: Mathematical Logic by George Tourlakis

Answer 1

You need the following result: $\vdash A \equiv A$ (see page 47).

With it, you can complete your proof:

1) $⊤ ≡ (⊥≡⊥)$ --- Axiom

2) $⊥≡⊥$ --- result above

3) $⊤$ --- from 1) and 2) by (Eqn): $\dfrac {A, A \equiv B}{B}$,

the "equational-style" version of Modus Ponens.