dfbi3 Show Code edit
# An alternate definition of the biconditional. Theorem *5.23 of
# [bib/WhiteheadRussell] p. 124.
## An alternative definition of biconditional
##
## See def-bi for more information.
##
thm (dfbi3 () () (<-> (<-> ph ps) (\/ (/\ ph ps) (/\ (-. ph) (-. ps)))) ph ps pm5.18 ph ps imnan ps ph con1b (-. ph) ps iman bitri anbi12i ph (-. ps) dfbi2 (/\ ph ps) (/\ (-. ph) (-. ps)) ioran 3bitr4ri con1bii bitri)
(<-> (<-> ph ps) (\/ (/\ ph ps) (/\ (-. ph) (-. ps))))
edit