mpbiran2 Show Code edit
# Detach truth from conjunction in biconditional.
thm (mpbiran2 () (mpbiran.1 (<-> ph (/\ ps ch)) mpbiran2.2 ch) (<-> ph ps) mpbiran.1 mpbiran2.2 ps biantru bitr4i)
(<-> ph ps)
edit