bibi2i Show Code edit
# Inference adding a biconditional to the left in an equivalence.
## Add biconditional to both sides of a equivalence
##
## (<-> [ ph ] [ [ ps)
## (<-> (-> ch [ ph ] ) [ (-> ch [ ps))
##
thm (bibi2i () (bibi.a (<-> ph ps)) (<-> (<-> ch ph) (<-> ch ps)) ch ph dfbi2 bibi.a ch imbi1i (-> ch ph) anbi2i bibi.a ch imbi2i (-> ps ch) anbi1i ch ps dfbi2 bitr4i 3bitri)
(<-> (<-> ch ph) (<-> ch ps))
edit