| ⊢ 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
We can easily combine this with theorem StateChopExportA to deduce the equivalence below: