oranabs Show Code edit
# Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton
# 23-Jun-2005.)
## Absorb redundant disjunct
thm (oranabs () () (<-> (/\ (\/ ph (-. ps)) ps) (/\ ph ps)) ph (-. ps) pm5.61 ps notnot (\/ ph (-. ps)) anbi2i ps notnot ph anbi2i 3bitr4i)
(<-> (/\ (\/ ph (-. ps)) ps) (/\ ph ps))
edit