| ⊢ | (f ⊃ fin w) ≡ f w | BiImpFinEqvYieldsState |
Proof:
1 | ⊢ (f ∧fin ¬w) ≡ f ; ¬w | |
2 | ⊢ f ∧fin ¬w ≡ f ∧¬fin w | |
3 | ⊢ f ∧¬fin w ≡¬(f ⊃ fin w) | |
4 | ⊢ f ∧fin ¬w ≡¬(f ⊃ fin w) | |
5 | ⊢ (f ∧fin ¬w) ≡¬(f ⊃ fin w) | |
6 | ⊢ ¬(f ⊃ fin w) ≡¬ (f ⊃ fin w) | |
7 | ⊢ ¬ (f ⊃ fin w) ≡ f ; ¬w | |
8 | ⊢ (f ⊃ fin w) ≡¬(f ; ¬w) | |
9 | ⊢ (f ⊃ fin w) ≡ f w | 8, def. of |
qed