biort Show Code edit
# A wff is disjoined with truth is true.
thm (biort () () (-> ph (<-> ph (\/ ph ps))) ph ps orc ph (\/ ph ps) ax-1 impbid2)
(-> ph (<-> ph (\/ ph ps)))
edit