bi3 Show Code edit
## Bicondition from two conditionals
thm (bi3 () () (-> (-> ph ps) (-> (-> ps ph) (<-> ph ps)))
(-> ph ps) (-> ps ph) and
(-> (-> ph ps) (-> (-> ps ph) (/\ (-> ph ps) (-> ps ph))))
ph ps def-bi-2
(-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps))
syl6)
(-> (-> ph ps) (-> (-> ps ph) (<-> ph ps)))
edit