| ⊢ | f ⊃ g, ⊢ f ; g ⊃ g ⇒ ⊢ f+ ⊃ g | ChopPlusElimWithoutMore |
Proof:
1 | ⊢ f ⊃ g | given |
2 | ⊢ f ; g ⊃ g | given |
3 | ⊢ (f ∧more) ; g ⊃ f ; g | |
4 | ⊢ (f ∧more) ; g ⊃ g | |
5 | ⊢ f+ ⊃ g |
qed