biorf Show Code edit
# A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of
# [bib/WhiteheadRussell] p. 121.
thm (biorf () () (-> (-. ph) (<-> ps (\/ ph ps))) (-. ph) ps biimt ph ps df-or syl6bbr)
(-> (-. ph) (<-> ps (\/ ph ps)))
edit