| ⊢ | w ∧ (f ; g) ⊃ (w ∧ f) ; g | StateAndChopImport |
Proof:
1 | ⊢ w ⊃ w | |
2 | ⊢ w ∧ (f ; g) ⊃ w ∧ (f ; g) | |
3 | ⊢ w ∧ (f ; g) ⊃ (w ∧ f) ; g | |
4 | ⊢ w ∧ (f ; g) ⊃ (w ∧ f) ; g |
qed
With this proved, we can easily combine it with theorem StateChopExportA to deduce the following equivalence: