带假设的mp规则（不可直接引用）
theorem _hyp_mp (A B G: wff): $ G \imp A \imp B $ > $ G \imp A $ > $ G \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mp_with_ant_thm | (G \imp A \imp B) \imp (G \imp A) \imp G \imp B |
|
| 2 | hyp h1 | G \imp A \imp B |
|
| 3 | 1, 2 | ax_mp | (G \imp A) \imp G \imp B |
| 4 | hyp h2 | G \imp A |
|
| 5 | 3, 4 | ax_mp | G \imp B |