| ⊢ | f ⊃ g ⇒ ⊢ f ⊃ g | NextImpNext |
Proof:
1 | ⊢ f ⊃ g | given |
2 | ⊢ (f ⊃ g) | |
3 | ⊢ (f ⊃ g) ⊃ (skip ; f) ⊃ (skip ; g) | |
4 | ⊢ (skip ; f) ⊃ (skip ; g) | |
5 | ⊢ f ⊃ g | 4, def. of |
qed