bianfd Show Code edit
# A wff conjoined with falsehood is false.
thm (bianfd () (bianfd.1 (-> ph (-. ps))) (-> ph (<-> ps (/\ ps ch))) bianfd.1 (/\ ps ch) pm2.21d ps ch pm3.26 impbid1)
(-> ph (<-> ps (/\ ps ch)))
edit