bianabs Show Code edit
# Absorb a hypothesis into the second member of a biconditional.
# (Contributed by FL, 15-Feb-2007.)
## Absorb antecedent
thm (bianabs () (bianabs.1 (-> ph (<-> ps (/\ ph ch)))) (-> ph (<-> ps ch)) bianabs.1 ph ch ibar bitr4d)
(-> ph (<-> ps ch))
edit