Step
*
of Lemma
contrapos1
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)})