\neg\imp合成
theorem negimp_comp (A B: wff): $ A \imp \neg B \imp \neg (A \imp B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | (A \imp (A \imp B) \imp B) \imp (((A \imp B) \imp B) \imp \neg B \imp \neg (A \imp B)) \imp A \imp \neg B \imp \neg (A \imp B) |
|
| 2 | imp_imp_swapl | ((A \imp B) \imp A \imp B) \imp A \imp (A \imp B) \imp B |
|
| 3 | imp_refl | (A \imp B) \imp A \imp B |
|
| 4 | 2, 3 | ax_mp | A \imp (A \imp B) \imp B |
| 5 | 1, 4 | ax_mp | (((A \imp B) \imp B) \imp \neg B \imp \neg (A \imp B)) \imp A \imp \neg B \imp \neg (A \imp B) |
| 6 | imp_introrev_neg | ((A \imp B) \imp B) \imp \neg B \imp \neg (A \imp B) |
|
| 7 | 5, 6 | ax_mp | A \imp \neg B \imp \neg (A \imp B) |