BiEqvBiBi

⊢ f ≡ f BiEqvBiBi

Proof:

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

qed

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