How to prove A→B is equivalent to ¬B→¬A? A→B is equivalent to ¬B→¬A This comes from a member called 6005 as an answer to my question: Why $F \rightarrow T \implies \neg F \rightarrow \neg T \implies T \rightarrow F$ is wrong?
Any proof or reference for this rule ?
 A: I believe you could simply check the truth table.
You have $4$ options:


*

*$A,B$ are true. In this case $A\rightarrow B$ is true because true implies true is true. and $\lnot B \rightarrow \lnot A$ is true because $\lnot B$ is false.

*$A,B$ are false. Then $\lnot A ,\lnot B$ are true so the same argument as above works.

*$A$ is true but $B$ is false. so $A\rightarrow B$ is false (as true implies false is false). Moreover $\lnot B \rightarrow \lnot A$ is also false because $\lnot B$ is true and $\lnot A$ is false.

*$A$ is false and $B$ is true. Then $A\rightarrow B$ is true because $A$ is false and $\lnot B\rightarrow \lnot A$ is true because $\lnot B$ is false.
A: Basic argument from first principles is like this. Assume $A \implies B$, and $B$ is not true. If $A$ is true, then $A \implies B$ so $B$ is true, which contradicts $B$ is not true. Hence, $A$ must be false.
In other words, $(A\implies B) \implies (\lnot B \implies \lnot A).$ 
The other way is just a negation in the above identity.
A: The implication $\neg B \Rightarrow \neg A$ is called the contrapositive of $A \Rightarrow B$.


*

*The fact that $A \Rightarrow B$ entails $\neg B \Rightarrow \neg A$ is valid even in constructive logic: suppose $A \Rightarrow B$ is true, and assume $\neg B$. If $A$ were true, then $B$ would be true by modus ponens (implication elimination), and so we obtain the contradiction $B \wedge \neg B$. Thus $\neg A$ is true. Hence $\neg B \Rightarrow \neg A$ is true by implication introduction.

*The fact that $\neg B \Rightarrow \neg A$ entails $A \Rightarrow B$ relies on double negation elimination: suppose $\neg B \Rightarrow \neg A$ is true, and assume $A$. If $\neg B$ were true, then $\neg A$ would be true by modus ponens, so we obtain the contradiction $A \wedge \neg A$. Thus $\neg \neg B$ is true, so that $B$ is true by double negation elimination. Hence $A \Rightarrow B$ is true by implication introduction.
Since $A \Rightarrow B$ entails and is entailed by $\neg B \Rightarrow \neg A$, they are logically equivalent.
Of course, you could just check a truth table, but that would be boring :)
