Next Prev Up
NotDiFalse

⊢ ¬false NotDiFalse

Proof:

1
⊢ true ⊃true
StateImpBi
2
⊢ true
Prop
3
⊢ true
1, 2,MP
4
⊢ ¬¬true
3, def. of 
5
⊢ ¬true ≡false
Prop
6
⊢ ¬true ≡false
5,DiEqvDi
7
⊢ ¬false
4, 6,Prop

qed

Next Prev Up

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024