biorfi Show Code edit
# A wff is equivalent to its disjunction with falsehood.
thm (biorfi () (biorfi.1 (-. ph)) (<-> ps (\/ ps ph)) biorfi.1 ph ps biorf ax-mp ph ps orcom bitri)
(<-> ps (\/ ps ph))
edit