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