notnotr Show Code edit
## Double Negative
thm (notnotr () () (<-> (-. (-. ph)) ph)
ph dn
(-> (-. (-. ph)) ph)
ph dnr
(-> ph (-. (-. ph)))
impbii
(<-> (-. (-. ph)) ph)
)
edit