\neg\imp交换
theorem neg_imp_swap (A B: wff): $ (\neg A \imp B) \imp \neg B \imp A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | ((\neg A \imp B) \imp \neg A \imp \neg \neg B) \imp ((\neg A \imp \neg \neg B) \imp \neg B \imp A) \imp (\neg A \imp B) \imp \neg B \imp A |
|
| 2 | imp_imp_insl | (\neg A \imp B \imp \neg \neg B) \imp (\neg A \imp B) \imp \neg A \imp \neg \neg B |
|
| 3 | introl_imp | (B \imp \neg \neg B) \imp \neg A \imp B \imp \neg \neg B |
|
| 4 | negneg_intro | B \imp \neg \neg B |
|
| 5 | 3, 4 | ax_mp | \neg A \imp B \imp \neg \neg B |
| 6 | 2, 5 | ax_mp | (\neg A \imp B) \imp \neg A \imp \neg \neg B |
| 7 | 1, 6 | ax_mp | ((\neg A \imp \neg \neg B) \imp \neg B \imp A) \imp (\neg A \imp B) \imp \neg B \imp A |
| 8 | neg_imp_elimrev | (\neg A \imp \neg \neg B) \imp \neg B \imp A |
|
| 9 | 7, 8 | ax_mp | (\neg A \imp B) \imp \neg B \imp A |