→左¬置换
theorem imp_left_neg_permute (A B: wff): $ (\neg A \imp B) \imp \neg B \imp A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_trans_curried | ((\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_for_imp_left_insert | (\neg A \imp B \imp \neg \neg B) \imp (\neg A \imp B) \imp \neg A \imp \neg \neg B |
|
| 3 | imp_left_intro | (B \imp \neg \neg B) \imp \neg A \imp B \imp \neg \neg B |
|
| 4 | neg_neg_intro | B \imp \neg \neg B |
|
| 5 | 3, 4 | mp | \neg A \imp B \imp \neg \neg B |
| 6 | 2, 5 | mp | (\neg A \imp B) \imp \neg A \imp \neg \neg B |
| 7 | 1, 6 | mp | ((\neg A \imp \neg \neg B) \imp \neg B \imp A) \imp (\neg A \imp B) \imp \neg B \imp A |
| 8 | neg_in_imp_reverse_elim | (\neg A \imp \neg \neg B) \imp \neg B \imp A |
|
| 9 | 7, 8 | mp | (\neg A \imp B) \imp \neg B \imp A |