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