dfbi1 Show Code edit
## Bicondition Definition from primitive connectives
thm (dfbi1 () () (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))
ph ps def-bi'
(<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))
(-> ph ps) (-> ps ph) df-an
(<-> (/\ (-> ph ps) (-> ps ph)) (-. (-> (-> ph ps) (-. (-> ps ph)))))
bitri)
(<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))
edit