\neg\and分配\or
theorem neg_and_dist_or (A B: wff): $ \neg (A \and B) \iff \neg A \or \neg B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\neg \neg (A \imp \neg B) \iff A \imp \neg B) \imp (A \imp \neg B \iff \neg \neg A \imp \neg B) \imp (\neg \neg (A \imp \neg B) \iff \neg \neg A \imp \neg B) |
|
| 2 | iff_symm | (A \imp \neg B \iff \neg \neg (A \imp \neg B)) \imp (\neg \neg (A \imp \neg B) \iff A \imp \neg B) |
|
| 3 | negneg_alloc | A \imp \neg B \iff \neg \neg (A \imp \neg B) |
|
| 4 | 2, 3 | ax_mp | \neg \neg (A \imp \neg B) \iff A \imp \neg B |
| 5 | 1, 4 | ax_mp | (A \imp \neg B \iff \neg \neg A \imp \neg B) \imp (\neg \neg (A \imp \neg B) \iff \neg \neg A \imp \neg B) |
| 6 | iff_intror_imp | (A \iff \neg \neg A) \imp (A \imp \neg B \iff \neg \neg A \imp \neg B) |
|
| 7 | negneg_alloc | A \iff \neg \neg A |
|
| 8 | 6, 7 | ax_mp | A \imp \neg B \iff \neg \neg A \imp \neg B |
| 9 | 5, 8 | ax_mp | \neg \neg (A \imp \neg B) \iff \neg \neg A \imp \neg B |
| 10 | 9 | conv or | \neg \neg (A \imp \neg B) \iff \neg A \or \neg B |
| 11 | 10 | conv and | \neg (A \and B) \iff \neg A \or \neg B |