imor Show Code edit
## OR and → Equivalance
## right('Equivalence', '∨')
thm (imor () () (<-> (-> ph ps) (\/ (-. ph) ps))
ph notnot
(<-> ph (-. (-. ph)))
ps imbi1i
(<-> (-> ph ps) (-> (-. (-. ph)) ps))
(-. ph) ps df-or
(<-> (\/ (-. ph) ps) (-> (-. (-. ph)) ps))
bicomi
(<-> (-> (-. (-. ph)) ps) (\/ (-. ph) ps))
bitri
(<-> (-> ph ps) (\/ (-. ph) ps))
)
edit