| ⊢ | f ; g ∧ f (g ⊃ g1) ⊃ f ; g1 | ChopAndYieldsMP |
Proof:
1 | ⊢ f ; g ∧ f (g ⊃ g1) ⊃ f ; (g ∧ (g ⊃ g1)) | |
2 | ⊢ g ∧ (g ⊃ g1) ⊃ g1 | |
3 | ⊢ f ; (g ∧ (g ⊃ g1)) ⊃ f ; g1 | |
4 | ⊢ f ; g ∧ f (g ⊃ g1) ⊃ f ; g1 |
qed