orel1 Show Code edit
## Denial of a Disjunct
## Elimination of disjunction by denying a disjunct. <.summary>
thm (orel1 () () (-> (-. ph) (-> (\/ ph ps) ps))
ph ps df-or
(<-> (\/ ph ps) (-> (-. ph) ps))
biimpi
(-> (\/ ph ps) (-> (-. ph) ps))
com12
(-> (-. ph) (-> (\/ ph ps) ps))
)
edit