Step
*
of Lemma
contrapos
P,Q:
.
({P
Q}
{(
Q)
(
P)})
BY
{
(Unfold
`guard`
0
THEN
Auto)
}
\mforall{}P,Q:\mBbbP{}. (\{P {}\mRightarrow{} Q\} {}\mRightarrow{} \{(\mneg{}Q) {}\mRightarrow{} (\mneg{}P)\})
By
(Unfold `guard` 0 THEN Auto)
Home
Index
P,Q:
. ({P 
Q} {(
Q) (P)})