Nuprl - Pf demorgan 1 1

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

At: demorgan 1 1

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

(P Q) P & Q

By: Analyze 3 THEN Analyze 4

Generated subgoals:

1 3. P
4. Q
5. (P Q)
P

2 3. P
4. Q
5. (P Q)
Q

3 3. P
4. Q
5. (P Q)
P

4 3. P
4. Q
5. (P Q)
Q

5 3. P
4. Q
5. P
6. Q
(P Q)

About:

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

1	3. `P` 4. `Q` 5. `(P Q)` `P`
2	3. `P` 4. `Q` 5. `(P Q)` `Q`
3	3. `P` 4. `Q` 5. `(P Q)` `P`
4	3. `P` 4. `Q` 5. `(P Q)` `Q`
5	3. `P` 4. `Q` 5. `P` 6. `Q` `(P Q)`