Next
Up
DfState
⊢
w
≡
w
DfState
Proof for
⊃
:
1
¬
w
⊃
¬
w
StateImpBf
2
¬
w
⊃ ¬
¬¬
w
1
,
def. of
3
¬¬
w
⊃
w
2
,
Prop
4
w
⊃ ¬¬
w
Prop
5
w
⊃
¬¬
w
4
,
DfImpDf
6
w
⊃
w
3
,
5
,
ImpChain
qed
Proof for
⊂
:
1
w
⊃
w
StateImpBf
2
w
⊃
w
BfImpDf
3
w
⊃
w
1
,
2
,
ImpChain
qed
Next
Up
2023-09-12
Contact
|
Home
|
ITL home
|
Course
|
Proofs
|
Algebra
|
FL
© 1996-2023