(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
contrapositive
1
1
2
1
1
1.
P:
Prop
2.
Q:
Prop
3.
P
P
4.
Q
5.
Q
P
6.
P
7.
P
Q
By:
UnfoldTopAb 7
THEN
FwdThru 7 [6]
THEN
Trivial
Generated subgoals:
None
About:
(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc