→中逆¬引出
theorem neg_in_imp_reverse_intro (A B: wff): $ (A \imp B) \imp \neg B \imp \neg A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_for_imp_right_reverse_intro | ((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_for_imp_right_reverse_intro | ((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_for_imp_right_reverse_intro | (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B |
|
| 4 | neg_neg_elim | \neg \neg A \imp A |
|
| 5 | 3, 4 | mp | (A \imp B) \imp \neg \neg A \imp B |
| 6 | 2, 5 | 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_for_imp_left_insert | (\neg \neg A \imp B \imp \neg \neg B) \imp (\neg \neg A \imp B) \imp \neg \neg A \imp \neg \neg B |
|
| 8 | imp_left_intro | (B \imp \neg \neg B) \imp \neg \neg A \imp B \imp \neg \neg B |
|
| 9 | neg_neg_intro | B \imp \neg \neg B |
|
| 10 | 8, 9 | mp | \neg \neg A \imp B \imp \neg \neg B |
| 11 | 7, 10 | mp | (\neg \neg A \imp B) \imp \neg \neg A \imp \neg \neg B |
| 12 | 6, 11 | mp | (A \imp B) \imp \neg \neg A \imp \neg \neg B |
| 13 | 1, 12 | 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_in_imp_reverse_elim | (\neg \neg A \imp \neg \neg B) \imp \neg B \imp \neg A |
|
| 15 | 13, 14 | mp | (A \imp B) \imp \neg B \imp \neg A |