| ⊢ | f ⊃ f1 ∨ f2 ⇒ ⊢ f ; g ⊃ (f1 ; g) ∨ (f2 ; g) | OrChopImpRule |
Proof:
1 | ⊢ f ⊃ f1 ∨ f2 | given |
2 | ⊢ f ; g ⊃ (f1 ∨ f2) ; g | |
3 | ⊢ (f ∨ f1) ; g ≡ f1 ; g ∨ f2 ; g | |
4 | ⊢ f ; g ⊃ (f1 ; g) ∨ (f2 ; g) |
qed