orri Show Code edit
## Infer implication from disjunction
thm (orri () (1 (-> (-. ph) ps)) (\/ ph ps)
1
(-> (-. ph) ps)
ph ps df-or
(<-> (\/ ph ps) (-> (-. ph) ps))
biimpri
(-> (-> (-. ph) ps) (\/ ph ps))
ax-mp
(\/ ph ps)
)
edit