BiEqvBi

⊢ f ≡ g ⇒ ⊢ f ≡ g BiEqvBi

Proof:

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

qed

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