def-bi' Show Code edit
## Alternative Definition of Biconditional
##
## See def-bi for more information. This is the same as
## See dfbi2.
##
thm (def-bi' () () (<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))
(<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))
edit