pm2.68 Show Code edit
## Unidirectional definition of OR
thm (pm2.68 () () (-> (-> (-> ph ps) ps) (\/ ph ps))
ph ps dfor2
(<-> (\/ ph ps) (-> (-> ph ps) ps))
biimpri
(-> (-> (-> ph ps) ps) (\/ ph ps))
)
edit