bianfi Show Code edit
# A wff conjoined with falsehood is false.
thm (bianfi () (bianfi.1 (-. ph)) (<-> ph (/\ ps ph)) bianfi.1 (/\ ps ph) pm2.21i ps ph pm3.27 impbii)
(<-> ph (/\ ps ph))
edit