| ⊢ | f ∧¬g ⊃ (more ; (f ∧¬g)) ⇒ ⊢ f ⊃ g | MoreChopContra |
Proof:
1 | ⊢ f ∧¬g ⊃ (more ; (f ∧¬g)) | given |
2 | ⊢ ¬(f ∧¬g) | |
3 | ⊢ f ⊃ g |
qed
Here is a variant of lemma MoreChopLoop that is useful in proofs: