NotDiEqvBiNot

⊢ ¬ f ≡¬f NotDiEqvBiNot

Proof:

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

qed

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