Nuprl - Pf demorgan2 1 1

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

At: demorgan2 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 Q

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

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

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

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

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

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

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

About:

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

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