¬消除→
theorem neg_elim_with_imp (A B: wff): $ \neg A \imp A \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_for_imp_left_insert | (\neg A \imp (\neg B \imp \neg A) \imp A \imp B) \imp (\neg A \imp \neg B \imp \neg A) \imp \neg A \imp A \imp B |
|
| 2 | imp_left_intro | ((\neg B \imp \neg A) \imp A \imp B) \imp \neg A \imp (\neg B \imp \neg A) \imp A \imp B |
|
| 3 | neg_in_imp_reverse_elim | (\neg B \imp \neg A) \imp A \imp B |
|
| 4 | 2, 3 | mp | \neg A \imp (\neg B \imp \neg A) \imp A \imp B |
| 5 | 1, 4 | mp | (\neg A \imp \neg B \imp \neg A) \imp \neg A \imp A \imp B |
| 6 | imp_left_intro | \neg A \imp \neg B \imp \neg A |
|
| 7 | 5, 6 | mp | \neg A \imp A \imp B |