Is $(P\implies Q)\implies (\lnot Q\implies \lnot P)$ always true? I've discovered that many theorems in mathematics are often in forms:
$$P\implies Q$$
I've also discovered that usually $\lnot Q\implies \lnot P$, if $P \implies Q$ is a theorem and I'm interested if this is always the case. So in language of mathematical logic, is the following statement always true:
$$(P\implies Q)\implies (\lnot Q\implies \lnot P)$$ 
 A: Informally, $P\Rightarrow Q$ is false when $P$ is true and $\neg Q$ is true. $\neg Q\Rightarrow\neg P$ is false when $\neg Q$ is true and $\neg(\neg P)=P$ is true. And so they're equivalent
Formally, using a truth table:
$$\begin{array}{|c|c|c|}\hline
P & Q & \color{}{P\Rightarrow Q} & \neg P & \neg Q & \color{}{\neg Q\Rightarrow\neg P}&\color{}{(P\Rightarrow Q)\Rightarrow(\neg Q\Rightarrow P)}\\ \hline
\color{green}1&\color{green}1&\color{green}1&\color{#C00}0&\color{#C00}0&\color{green}1&\color{green}1\\ \hline
\color{green}1&\color{#C00}0&\color{green}1&\color{#C00}0&\color{green}1&\color{green}1&\color{green}1\\ \hline
\color{#C00}0&\color{green}1&\color{#C00}0&\color{green}1&\color{#C00}0&\color{#C00}0&\color{green}1\\ \hline
\color{#C00}0&\color{#C00}0&\color{green}1&\color{green}1&\color{green}1&\color{green}1&\color{green}1\\ \hline
\end{array}$$
A: As commented on above, the two statements are logically equivalent. Here's a proof:
$$ \begin{align*} 
   (P\Rightarrow Q) 
 & \Leftrightarrow \lnot(P\land\lnot Q)\\
 & \Leftrightarrow \lnot\lnot\lnot(P\land\lnot Q) \\
 & \Leftrightarrow\lnot\lnot(Q\lor\lnot P) \\
 & \Leftrightarrow\lnot(\lnot Q\land\lnot\lnot P) \\
 & \Leftrightarrow (\lnot Q \Rightarrow \lnot P) 
\end{align*}
$$
A: Along the lines of Simon S's proof...
$[P\implies Q]\equiv \neg[P \land \neg Q]$
$[\neg Q\implies \neg P]\equiv \neg[\neg Q \land \neg\neg P] \equiv \neg[\neg Q \land  P]\equiv \neg[P \land \neg Q] $
