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