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