| ⊢ | g ⊃ g1 ∨ g2 ⇒ ⊢ f ; g ⊃ (f ; g1) ∨ (f ; g2) | ChopOrImpRule |
Proof:
1 | ⊢ g ⊃ g1 ∨ g2 | given |
2 | ⊢ f ; g ⊃ f ; (g1 ∨ g2) | |
3 | ⊢ f ; (g ∨ g) ≡ f ; g1 ∨ f ; g2 | |
4 | ⊢ f ; g ⊃ (f ; g1) ∨ (f ; g2) |
qed