\imp\and左插入\or
theorem imp_and_insl_or (A B C: wff): $ (A \imp B \and C) \imp (A \imp B) \or (A \imp C) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | ((A \imp B \and C) \imp (A \imp B) \and (A \imp C)) \imp ((A \imp B) \and (A \imp C) \imp (A \imp B) \or (A \imp C)) \imp (A \imp B \and C) \imp (A \imp B) \or (A \imp C) |
|
| 2 | imp_and_insl | (A \imp B \and C) \imp (A \imp B) \and (A \imp C) |
|
| 3 | 1, 2 | ax_mp | ((A \imp B) \and (A \imp C) \imp (A \imp B) \or (A \imp C)) \imp (A \imp B \and C) \imp (A \imp B) \or (A \imp C) |
| 4 | and_to_or | (A \imp B) \and (A \imp C) \imp (A \imp B) \or (A \imp C) |
|
| 5 | 3, 4 | ax_mp | (A \imp B \and C) \imp (A \imp B) \or (A \imp C) |