dfbi2 Show Code edit
# A theorem similar to the standard definition of the biconditional.
# Definition of [bib/Margaris] p. 49.
## Definition of biconditional
##
## See def-bi for more information.
##
## left('Simplify', '↔')
thm (dfbi2 () () (<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph))) ph ps dfbi1 (-> ph ps) (-> ps ph) df-an bitr4i)
(<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))
edit