\imp左引入\and
theorem imp_introl_and (A B C: wff): $ (A \imp B) \imp C \and A \imp C \and B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | ((A \imp B) \imp (C \imp \neg B) \imp C \imp \neg A) \imp (((C \imp \neg B) \imp C \imp \neg A) \imp \neg (C \imp \neg A) \imp \neg (C \imp \neg B)) \imp (A \imp B) \imp \neg (C \imp \neg A) \imp \neg (C \imp \neg B) |
|
| 2 | imp_tran | ((A \imp B) \imp \neg B \imp \neg A) \imp ((\neg B \imp \neg A) \imp (C \imp \neg B) \imp C \imp \neg A) \imp (A \imp B) \imp (C \imp \neg B) \imp C \imp \neg A |
|
| 3 | imp_introrev_neg | (A \imp B) \imp \neg B \imp \neg A |
|
| 4 | 2, 3 | ax_mp | ((\neg B \imp \neg A) \imp (C \imp \neg B) \imp C \imp \neg A) \imp (A \imp B) \imp (C \imp \neg B) \imp C \imp \neg A |
| 5 | imp_introl_imp | (\neg B \imp \neg A) \imp (C \imp \neg B) \imp C \imp \neg A |
|
| 6 | 4, 5 | ax_mp | (A \imp B) \imp (C \imp \neg B) \imp C \imp \neg A |
| 7 | 1, 6 | ax_mp | (((C \imp \neg B) \imp C \imp \neg A) \imp \neg (C \imp \neg A) \imp \neg (C \imp \neg B)) \imp (A \imp B) \imp \neg (C \imp \neg A) \imp \neg (C \imp \neg B) |
| 8 | imp_introrev_neg | ((C \imp \neg B) \imp C \imp \neg A) \imp \neg (C \imp \neg A) \imp \neg (C \imp \neg B) |
|
| 9 | 7, 8 | ax_mp | (A \imp B) \imp \neg (C \imp \neg A) \imp \neg (C \imp \neg B) |
| 10 | 9 | conv and | (A \imp B) \imp C \and A \imp C \and B |