orrd Show Code edit
## Deduce implication from disjunction
thm (orrd () (1 (-> ph (-> (-. ps) ch))) (-> ph (\/ ps ch))
1
(-> ph (-> (-. ps) ch))
ps ch df-or
(<-> (\/ ps ch) (-> (-. ps) ch))
biimpri
(-> (-> (-. ps) ch) (\/ ps ch))
syl
(-> ph (\/ ps ch))
)
edit