niabn Show Code edit
# Miscellaneous inference relating falsehoods.
thm (niabn () (niabn.1 ph) (-> (-. ps) (<-> (/\ ch ps) (-. ph))) ch ps pm3.27 niabn.1 ps pm2.24i pm5.21ni)
(-> (-. ps) (<-> (/\ ch ps) (-. ph)))
edit