oibabs Show Code edit
# Absorption of disjunction into equivalence.
## Absorb disjunction
thm (oibabs () () (<-> (-> (\/ ph ps) (<-> ph ps)) (<-> ph ps)) ph ps orc (<-> ph ps) imim1i ibd ps ph olc (<-> ph ps) imim1i ps ph ibibr sylibr impbid (<-> ph ps) (\/ ph ps) ax-1 impbii)
(<-> (-> (\/ ph ps) (<-> ph ps)) (<-> ph ps))
edit