1\DOC CONTRAPOS_CONV 2 3\TYPE {CONTRAPOS_CONV : conv} 4 5\SYNOPSIS 6Proves the equivalence of an implication and its contrapositive. 7 8\KEYWORDS 9conversion, contrapositive, implication. 10 11\DESCRIBE 12When applied to an implication {P ==> Q}, the conversion {CONTRAPOS_CONV} 13returns the theorem: 14{ 15 |- (P ==> Q) = (~Q ==> ~P) 16} 17 18 19\FAILURE 20Fails if applied to a term that is not an implication. 21 22\SEEALSO 23Drule.CONTRAPOS. 24\ENDDOC 25