Next Prev Up
BoxEqvBox

⊢ f ≡ g ⇒ ⊢ f ≡ g BoxEqvBox

Proof:

1
f ≡ g
Assump
2
¬f ≡¬g
1,Prop
3
¬f ≡¬g
2,DiamondEqvDiamond
4
¬¬f ≡¬¬g
3,Prop
5
f ≡ g
4, def. of 

qed

Next Prev Up

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