| ⊢ | f ∧¬g ⊃ h ; f ∧¬(h ; g), ⊢ h ⊃ more ⇒ ⊢ f ⊃ g | ChopContra |
Proof:
1 | ⊢ f ∧¬g ⊃ h ; f ∧¬(h ; g) | given |
2 | ⊢ h ⊃more | given |
3 | ⊢ h ; f ∧¬(h ; g) ⊃ h ; (f ∧¬g) | |
4 | ⊢ h ; (f ∧¬g) ⊃more ; (f ∧¬g) | |
5 | ⊢ f ∧¬g ⊃more ; (f ∧¬g) | |
6 | ⊢ f ⊃ g |
qed