| CURRENT LINE NUMBER | DEPENDS ON | CURRENT LINE | DERIVED BY |
| 1. | 1 | ¬ (P v Q) | Assumption [discharged line 11] |
| 2. | 2 | P | Assumption [discharged line 5] |
| 3. | 2 | P v Q | 2, vI |
| 4. | 1, 2 | (P v Q) & ¬ (P v Q) | 1, 3 &I |
| 5. | 1 | ¬ P | 2, 4 ¬I |
| 6. | 6 | Q | Assumption [discharged line 9] |
| 7. | 6 | P v Q | 6, vI |
| 8. | 1, 6 | (P v Q) & ¬ (P v Q) | 1, 7, &I |
| 9. | 1 | ¬ Q | 6, 8 ¬I |
| 10. | 1 | ¬ P & ¬ Q | 5, 9 &I |
| 11. | ¬ (P v Q) ⊃ ¬ P & ¬ Q | 1, 10 ⊃I | |
| 12. | 12 | ¬ P & ¬ Q | Assumption [discharged line 24] |
| 13. | 12 | ¬ P | 12 &E |
| 14. | 14 | P v Q | Assumption [discharged line 24] |
| 15. | 15 | P | Assumption [discharged line 21] |
| 16. | 16 | ¬ Q | Assumption [discharged line 18] |
| 17. | 12, 15 | P & ¬ P | 12, 15 &I |
| 18. | 12, 15 | ¬ ¬ Q | 16,17 ¬I |
| 19. | 12, 15 | Q | 18 ¬E |
| 20. | 20 | Q | Assumption [discharged line 21] |
| 21. | 12, 14 | Q | 14, 15, 19, 20, 20 vE |
| 22. | 12 | ¬ Q | 12, &E |
| 23. | 12, 14 | Q & ¬ Q | 21, 22 &I |
| 24. | 12 | ¬ (P v Q) | 14, 23 ¬E |
| 25. | ¬ P & ¬ Q ⊃ ¬ (P v Q) | 12, 24 ⊃I | |
| 26. | (¬ (P v Q) ⊃ ¬ P & ¬ Q) | ||
| & (¬ P & ¬ Q ⊃ ¬ (P v Q)) | 11, 25 &I | ||
| 27. | ¬ P & ¬ Q ≡ ¬ (P v Q) | 26 ≡I |