Nuprl - Pf contrapositive 1 1

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

At: contrapositive 1 1

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

(P Q) (Q P)

By: Analyze 0 THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 5. P Q
6. Q
P

2 5. Q P
6. P
Q

About:

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