Next Prev Up
NotDiEqvBiNot

⊢ ¬ f ≡¬f NotDiEqvBiNot

Proof:

1
⊢ f ≡¬¬f
Prop
2
⊢ f ≡¬¬f
1,DiEqvDi
3
⊢ ¬ f ≡¬¬¬f
2,Prop
4
⊢ ¬ f ≡¬f
3, def. of 

qed

Next Prev Up

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023