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