orel2 Show Code edit
## Denial of a Disjunct
## Elimination of disjunction by denying a disjunct. <.summary>
thm (orel2 () () (-> (-. ph) (-> (\/ ps ph) ps))
ph ps orel1
(-> (-. ph) (-> (\/ ph ps) ps))
ps ph orcom
(<-> (\/ ps ph) (\/ ph ps))
syl5ib
(-> (-. ph) (-> (\/ ps ph) ps))
)
edit