pm2.54 Show Code edit
## Infer Disjunction
thm (pm2.54 () () (-> (-> (-. ph) ps) (\/ ph ps))
ph ps df-or
(<-> (\/ ph ps) (-> (-. ph) ps))
biimpri
(-> (-> (-. ph) ps) (\/ ph ps))
)
edit