pm5.19 Show Code edit
# Theorem *5.19 of [bib/WhiteheadRussell] p. 124.
## An proposition is not equivalence to its negation
thm (pm5.19 () () (-. (<-> ph (-. ph))) ph biid ph ph pm5.18 mpbi)
(-. (<-> ph (-. ph)))
edit