oridm Show Code edit
## Disjunction is Idempotent
## right('Simplify', '∨')
thm (oridm () () (<-> (\/ ph ph) ph)
ph ph df-or
(<-> (\/ ph ph) (-> (-. ph) ph))
ph pm4.81
(<-> (-> (-. ph) ph) ph)
bitri
(<-> (\/ ph ph) ph)
)
edit