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