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