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