Nuprl - Pf contrapositive 1 1 1 1

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

At: contrapositive 1 1 1 1

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

P

By: FwdThru 5 [3]

Generated subgoal:

1 7. Q
P

About:

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