\imp右插入
theorem imp_imp_insr (A B C: wff): $ ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_introrsl_imp | (((A \imp B) \imp C) \imp B \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C |
|
| 2 | imp_tran | (((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp ((B \imp (A \imp B) \imp C) \imp B \imp C) \imp ((A \imp B) \imp C) \imp B \imp C |
|
| 3 | introl_imp | ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C |
|
| 4 | 2, 3 | ax_mp | ((B \imp (A \imp B) \imp C) \imp B \imp C) \imp ((A \imp B) \imp C) \imp B \imp C |
| 5 | imp_imp_elimrsl | ((B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp (B \imp A \imp B) \imp (B \imp (A \imp B) \imp C) \imp B \imp C |
|
| 6 | imp_imp_insl | (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C |
|
| 7 | 5, 6 | ax_mp | (B \imp A \imp B) \imp (B \imp (A \imp B) \imp C) \imp B \imp C |
| 8 | introl_imp | B \imp A \imp B |
|
| 9 | 7, 8 | ax_mp | (B \imp (A \imp B) \imp C) \imp B \imp C |
| 10 | 4, 9 | ax_mp | ((A \imp B) \imp C) \imp B \imp C |
| 11 | 1, 10 | ax_mp | ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C |