| ⊢ (skip ⊃ f) ∧ g ⊃ (skip ∧ f) ⌢ g | BfSkipImpAndNextImpAndSkipAndChop |
Proof:
1 | (skip ⊃ f) ∧ (skip ⌢ g) ⊃ ((skip ⊃ f) ∧skip) ⌢ g | |
2 | (skip ⊃ f) ∧skip ⊃ skip ∧ f | |
3 | ((skip ⊃ f) ∧skip) ⌢ g ⊃ (skip ∧ f) ⌢ g | |
4 | (skip ⊃ f) ∧ (skip ⌢ g) ⊃ (skip ∧ f) ⌢ g | |
5 | (skip ⊃ f) ∧ g ⊃ (skip ∧ f) ⌢ g | 4, def. of |
qed