\iff\neg置换
theorem iff_neg_perm (A B: wff): $ (A \iff \neg B) \iff B \iff \neg A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_simintro_and | (A \imp \neg B \iff B \imp \neg A) \imp (\neg B \imp A \iff \neg A \imp B) \imp ((A \imp \neg B) \and (\neg B \imp A) \iff (B \imp \neg A) \and (\neg A \imp B)) |
|
| 2 | imp_neg_perm | A \imp \neg B \iff B \imp \neg A |
|
| 3 | 1, 2 | ax_mp | (\neg B \imp A \iff \neg A \imp B) \imp ((A \imp \neg B) \and (\neg B \imp A) \iff (B \imp \neg A) \and (\neg A \imp B)) |
| 4 | neg_imp_perm | \neg B \imp A \iff \neg A \imp B |
|
| 5 | 3, 4 | ax_mp | (A \imp \neg B) \and (\neg B \imp A) \iff (B \imp \neg A) \and (\neg A \imp B) |
| 6 | 5 | conv iff | (A \iff \neg B) \iff B \iff \neg A |