Derive each negated component in its own subproof, then combine them. Assumption lines below begin local scopes; the listed discharge ranges close those scopes.
| Line | Formula | Justification |
|---|---|---|
| 1 | Premise | |
| 2 | Assume locally | |
| 3 | Disjunction introduction rule, left, 2 | |
| 4 | Negation elimination rule, 1 and 3 | |
| 5 | Negation introduction rule, discharging 2–4 | |
| 6 | Assume locally | |
| 7 | Disjunction introduction rule, right, 6 | |
| 8 | Negation elimination rule, 1 and 7 | |
| 9 | Negation introduction rule, discharging 6–8 | |
| 10 | Conjunction introduction rule, 5 and 9 |
Only the original premise remains open. No classical principle is needed for this direction of De Morgan's laws.
Articles by others on the same topic
There are currently no matching articles.