Nuprl - Pf decidable functionality wrt iff 1

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

At: decidable functionality wrt iff 1

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

Q Q

By: Analyze 5

Generated subgoals:

1 5. P
Q Q

2 5. P
Q Q

About:

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