矛盾律
theorem contradiction (A: wff): $ \neg (A \and \neg A) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neg_neg_intro | (A \imp \neg \neg A) \imp \neg \neg (A \imp \neg \neg A) |
|
| 2 | neg_neg_intro | A \imp \neg \neg A |
|
| 3 | 1, 2 | mp | \neg \neg (A \imp \neg \neg A) |
| 4 | 3 | conv and | \neg (A \and \neg A) |