bibi1i Show Code edit
# Inference adding a biconditional to the right in an equivalence.
## Add biconditional to both sides of a equivalence
##
## (<-> ph ] ] [ ps ] )
## (<-> (<-> ph ] ch) ] (<-> [ ps ] ch))
##
thm (bibi1i () (bibi.a (<-> ph ps)) (<-> (<-> ph ch) (<-> ps ch)) ph ch bicom bibi.a ch bibi2i ch ps bicom 3bitri)
(<-> (<-> ph ch) (<-> ps ch))
edit