| ⊢ | f ; g ∧ f g1 ⊃ f ; (g ∧ g1) | ChopAndYieldsImp |
This shows how yields adds information to the right of a suitable chop formula.
Proof:
1 | ⊢ g ⊃ (g ∧ g1) ∨¬g1 | |
2 | ⊢ f ; g ⊃ f ; (g ∧ g1) ∨ f ; ¬g1 | |
3 | ⊢ f ; g ∧¬(f ; ¬g1) ⊃ f ; (g ∧ g1) | |
4 | ⊢ f ; g ∧ f g1 ⊃ f ; (g ∧ g1) | 3, def. of |
qed
Here is a corollary: