Nuprl - Pf contrapositive 1 1 2

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

At: contrapositive 1 1 2

1. P: Prop
2. Q: Prop
3. P P
4. Q Q
5. Q P
6. P

Q

By: Analyze 4

Generated subgoal:

1 4. Q
5. Q P
6. P
Q

About:

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