| ⊢ | f ∧¬g ⊃ (g ∧more) ; f ⇒ ⊢ f ⊃ g+ | ChopPlusIntro |
Proof:
1 | ⊢ f ∧¬g ⊃ (g ∧more) ; f | given |
2 | ⊢ g+ ≡ g ∨ (g ∧more) ; g+ | |
3 | ⊢ f ∧¬(g+) ⊃ (g ∧more) ; f ∧¬((g ∧more) ; g+) | |
4 | ⊢ g ∧more ⊃more | |
5 | ⊢ f ⊃ g+ |
qed