Given the premises p→q and ¬p→¬q, prove that p is logically equivalent to q Given the premises p→q and ¬p→¬q, prove that p is logically equivalent to q.
I understand why this works, but I do not know how to construct a complete formal proof. So far, I have this:
premises:
p→q ¬p→¬q 
(p→q) ∧ (¬p→¬q) ⇔ T
apply contrapositive law
(p→q) ∧ (q→p) ⇔ T
∴ (p↔q) ⇔ T

At this point, how do I formally assert (using symbols and laws) that, because (p↔q) is a tautology, p and q must be logically equivalent to each other?

Hint:
To prove this use natural deduction, in general we will use $\leftrightarrow\text{ Intro }$, so we want to first assume $Q$, see if this indeed implies $P$, another direction is trivial by $\to\text{ Elim }$ from $P\to Q$.
Answer:
$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{1.~P\to Q\\2.~\neg P\to \neg Q}{\fitch{3.~Q}{\fitch{4.~\neg P}{5.~\neg Q\hspace{10ex}\to\text{ Elim }2,4\\6.~\bot\hspace{12.5ex}\bot\text{ Intro }3,5}\\7.~\neg\neg P\hspace{13.2ex}\neg\text{ Intro }4-6\\8.~P\hspace{16.2ex}\neg\neg\text{ Elim }7}\\\fitch{9.~P}{10.~Q\hspace{14.5ex}\to\text{ Elim }1,9}\\11.~P\leftrightarrow Q\hspace{12.5ex}\leftrightarrow\text{ Intro }3-8,9-10}$$


$\underline{\text{Definition}}$
  Formulas $P$ and $Q$ are logically equivalent if and only if the statement of their material equivalence $(P\leftrightarrow Q)$ is a tautology.
  (There is a difference between being true and being a tautology)

If we have premise says $P\to Q$ and $\neg P\to\neg Q$ are tautology this is reasonable: 
$$\begin{align}
1.~&P\to Q\equiv \top&&\text{Premise}\\
2.~&\neg P\to \neg Q\equiv \top&&\text{Premise}\\
3.~&Q\to P\equiv \top&&\text{Contrapositive 2}\\
4.~&P\to Q\land Q\to P\equiv\top\land\top\equiv \top&&\text{Domination law 1,3}\\
5.~&P\leftrightarrow Q\equiv\top&&\text{Biconditional equivalence 4}\\
6.~&P\equiv Q&&\text{Definition 5}
\end{align}$$
However if the premise only says $P\to Q$ and $\neg P\to\neg Q$ are true, we only know that $P\leftrightarrow Q$ is also true, which might not be a tautology.
