I've started to work through Applied Mathematics for Database Professionals and have been stuck on one of the exercises for two days. I've been able to prove the expression: $$\left( P\Rightarrow Q \right) \Leftrightarrow \left( \neg Q \Rightarrow \neg P \right)$$ is true using a truth table but can't make the leap using rewrite rules.
Starting with the implication: $$ P \Rightarrow Q$$ Rewrite implication into disjunction: $$\neg P \vee Q $$ By commutativity the expression becomes: $$ Q \vee \neg P $$ Via double negation: $$ \neg \neg Q \vee \neg P $$ This is where I get stuck. The answer in the book shows rewriting the expression back into an implication: $$ \neg Q \Rightarrow \neg P $$ I understand where the $ \neg P $ comes from, it's from the initial rewrite rule. My confusion is, how is the $ \neg Q $ derived?