(9steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

At: contrapositive 1 1 1 1 1
1. P: Prop
2. Q: Prop
3. P
4. Q Q
5. P Q
6. Q
7. Q

P
By:
UnfoldTopAb 6
THEN
FwdThru 6 [7]
THEN
Trivial
Generated subgoals:

None

About:
propimpliesor

(9steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc