dfbi Show Code edit
## Definition of biconditional
##
## Definition [[df-bi]] rewritten in an abbreviated form to help intuitive
## understanding of that definition. Note that it is a conjunction of
## two implications; one which asserts properties that follow from the
## biconditional and one which asserts properties that imply the
## biconditional.
##
thm (dfbi () () (/\ (-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph))) (-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps))) ph ps dfbi2 biimpi ph ps dfbi2 biimpri pm3.2i)
(/\ (-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph))) (-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps)))
edit