anbi2i Show Code edit
## Add conjunct to both sides
## Introduce a left conjunct to both sides of a logical equivalence.
##
## (<-> [ ph ] [ [ ps)
## (<-> (/\ ch [ ph ] ) [ (/\ ch [ ps))
##
thm (anbi2i () (bi.aa (<-> ph ps)) (<-> (/\ ch ph) (/\ ch ps)) bi.aa biimpi ch anim2i bi.aa biimpri ch anim2i impbii)
(<-> (/\ ch ph) (/\ ch ps))
edit