\imp左矛盾消去
theorem imp2_elimcontradl (A B: wff): $ (A \imp B) \imp (\neg A \imp B) \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_imp_swapl | ((\neg A \imp B) \imp (A \imp B) \imp B) \imp (A \imp B) \imp (\neg A \imp B) \imp B |
|
| 2 | imp_tran | ((((A \imp A) \imp B) \imp B) \imp ((A \imp B) \imp (A \imp A) \imp B) \imp (A \imp B) \imp B) \imp
((((A \imp B) \imp (A \imp A) \imp B) \imp (A \imp B) \imp B) \imp
((\neg A \imp B) \imp (A \imp B) \imp (A \imp A) \imp B) \imp
(\neg A \imp B) \imp
(A \imp B) \imp
B) \imp
(((A \imp A) \imp B) \imp B) \imp
((\neg A \imp B) \imp (A \imp B) \imp (A \imp A) \imp B) \imp
(\neg A \imp B) \imp
(A \imp B) \imp
B |
|
| 3 | imp_introl_imp | (((A \imp A) \imp B) \imp B) \imp ((A \imp B) \imp (A \imp A) \imp B) \imp (A \imp B) \imp B |
|
| 4 | 2, 3 | ax_mp | ((((A \imp B) \imp (A \imp A) \imp B) \imp (A \imp B) \imp B) \imp
((\neg A \imp B) \imp (A \imp B) \imp (A \imp A) \imp B) \imp
(\neg A \imp B) \imp
(A \imp B) \imp
B) \imp
(((A \imp A) \imp B) \imp B) \imp
((\neg A \imp B) \imp (A \imp B) \imp (A \imp A) \imp B) \imp
(\neg A \imp B) \imp
(A \imp B) \imp
B |
| 5 | imp_introl_imp | (((A \imp B) \imp (A \imp A) \imp B) \imp (A \imp B) \imp B) \imp ((\neg A \imp B) \imp (A \imp B) \imp (A \imp A) \imp B) \imp (\neg A \imp B) \imp (A \imp B) \imp B |
|
| 6 | 4, 5 | ax_mp | (((A \imp A) \imp B) \imp B) \imp ((\neg A \imp B) \imp (A \imp B) \imp (A \imp A) \imp B) \imp (\neg A \imp B) \imp (A \imp B) \imp B |
| 7 | mp_with_ant_thm | (((A \imp A) \imp B) \imp (A \imp A) \imp B) \imp (((A \imp A) \imp B) \imp A \imp A) \imp ((A \imp A) \imp B) \imp B |
|
| 8 | mp_thm | ((A \imp A) \imp B) \imp (A \imp A) \imp B |
|
| 9 | 7, 8 | ax_mp | (((A \imp A) \imp B) \imp A \imp A) \imp ((A \imp A) \imp B) \imp B |
| 10 | introl_imp | (A \imp A) \imp ((A \imp A) \imp B) \imp A \imp A |
|
| 11 | imp_refl | A \imp A |
|
| 12 | 10, 11 | ax_mp | ((A \imp A) \imp B) \imp A \imp A |
| 13 | 9, 12 | ax_mp | ((A \imp A) \imp B) \imp B |
| 14 | 6, 13 | ax_mp | ((\neg A \imp B) \imp (A \imp B) \imp (A \imp A) \imp B) \imp (\neg A \imp B) \imp (A \imp B) \imp B |
| 15 | neg_imp_with_imp_mergel_imp | (\neg A \imp B) \imp (A \imp B) \imp (A \imp A) \imp B |
|
| 16 | 14, 15 | ax_mp | (\neg A \imp B) \imp (A \imp B) \imp B |
| 17 | 1, 16 | ax_mp | (A \imp B) \imp (\neg A \imp B) \imp B |