def-bi-2 Show Code edit
## Two Conditionals Implies Biconditional
thm (def-bi-2 () () (-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps))
ph ps def-bi and2i)
(-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps))
edit