\imp对\imp左折叠
theorem imp_imp_foldl (A B: wff): $ A \imp A \imp B \iff A \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | ((A \imp A \imp B) \imp A \imp B) \imp ((A \imp B) \imp A \imp A \imp B) \imp (A \imp A \imp B \iff A \imp B) |
|
| 2 | imp_imp_assiml | (A \imp A \imp B) \imp A \imp B |
|
| 3 | 1, 2 | ax_mp | ((A \imp B) \imp A \imp A \imp B) \imp (A \imp A \imp B \iff A \imp B) |
| 4 | introl_imp | (A \imp B) \imp A \imp A \imp B |
|
| 5 | 3, 4 | ax_mp | A \imp A \imp B \iff A \imp B |