(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:
propimpliesor

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