| ⊢ (more ⊃ T) ≡more ⊃ T | BfMoreImpNLoneEqvMoreImpNLone |
Proof:
1 | (more ⊃ T) ≡¬¬(more ⊃ T) | def. of |
2 | ¬(more ⊃ T) ≡more ∧¬T | |
3 | ¬(more ⊃ T) ≡ (more ∧¬T) | |
4 | (more ∧¬T) ≡more ∧¬T | |
5 | ¬(more ⊃ T) ≡more ∧¬T | |
6 | (more ⊃ T) ≡¬(more ∧¬T) | |
7 | ¬(more ∧¬T) ≡more ⊃ T | |
8 | (more ⊃ T) ≡more ⊃ T |
qed