\imp逆引入\neg
theorem imp_introrev_neg (A B: wff): $ (A \imp B) \imp \neg B \imp \neg A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_introrevr_imp | ((A \imp B) \imp \neg \neg A \imp \neg \neg B) \imp ((\neg \neg A \imp \neg \neg B) \imp \neg B \imp \neg A) \imp (A \imp B) \imp \neg B \imp \neg A |
|
| 2 | imp_introrevr_imp | ((A \imp B) \imp \neg \neg A \imp B) \imp ((\neg \neg A \imp B) \imp \neg \neg A \imp \neg \neg B) \imp (A \imp B) \imp \neg \neg A \imp \neg \neg B |
|
| 3 | imp_introrevr_imp | (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B |
|
| 4 | negneg_elim | \neg \neg A \imp A |
|
| 5 | 3, 4 | ax_mp | (A \imp B) \imp \neg \neg A \imp B |
| 6 | 2, 5 | ax_mp | ((\neg \neg A \imp B) \imp \neg \neg A \imp \neg \neg B) \imp (A \imp B) \imp \neg \neg A \imp \neg \neg B |
| 7 | imp_imp_insl | (\neg \neg A \imp B \imp \neg \neg B) \imp (\neg \neg A \imp B) \imp \neg \neg A \imp \neg \neg B |
|
| 8 | introl_imp | (B \imp \neg \neg B) \imp \neg \neg A \imp B \imp \neg \neg B |
|
| 9 | negneg_intro | B \imp \neg \neg B |
|
| 10 | 8, 9 | ax_mp | \neg \neg A \imp B \imp \neg \neg B |
| 11 | 7, 10 | ax_mp | (\neg \neg A \imp B) \imp \neg \neg A \imp \neg \neg B |
| 12 | 6, 11 | ax_mp | (A \imp B) \imp \neg \neg A \imp \neg \neg B |
| 13 | 1, 12 | ax_mp | ((\neg \neg A \imp \neg \neg B) \imp \neg B \imp \neg A) \imp (A \imp B) \imp \neg B \imp \neg A |
| 14 | neg_imp_elimrev | (\neg \neg A \imp \neg \neg B) \imp \neg B \imp \neg A |
|
| 15 | 13, 14 | ax_mp | (A \imp B) \imp \neg B \imp \neg A |