Nuprl - Pf decidable functionality wrt iff 2 2 1 1

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

At: decidable functionality wrt iff 2 2 1 1

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

False

By: FwdThru 3 [6]

Generated subgoal:

1 7. Q
False

About:

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