orabs Show Code edit
# Absorption of redundant internal disjunct. Compare Theorem *4.45
# of [bib/WhiteheadRussell] p. 119.
## Absorb redundant disjunct
thm (orabs () () (<-> ph (/\ (\/ ph ps) ph)) ph ps orc ancri (\/ ph ps) ph pm3.27 impbii)
(<-> ph (/\ (\/ ph ps) ph))
edit