\imp\neg置换
theorem imp_neg_perm (A B: wff): $ A \imp \neg B \iff B \imp \neg A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | ((A \imp \neg B) \imp B \imp \neg A) \imp ((B \imp \neg A) \imp A \imp \neg B) \imp (A \imp \neg B \iff B \imp \neg A) |
|
| 2 | imp_neg_swap | (A \imp \neg B) \imp B \imp \neg A |
|
| 3 | 1, 2 | ax_mp | ((B \imp \neg A) \imp A \imp \neg B) \imp (A \imp \neg B \iff B \imp \neg A) |
| 4 | imp_neg_swap | (B \imp \neg A) \imp A \imp \neg B |
|
| 5 | 3, 4 | ax_mp | A \imp \neg B \iff B \imp \neg A |