anbi1i Show Code edit
## Add conjunct to both sides
## Introduce a right conjunct to both sides of a logical equivalence.
##
## (<-> ph ] ] [ ps ] )
## (<-> (/\ ph ] ch) ] (/\ [ ps ] ch))
##
thm (anbi1i () (bi.aa (<-> ph ps)) (<-> (/\ ph ch) (/\ ps ch)) ph ch ancom bi.aa ch anbi2i ch ps ancom 3bitri)
(<-> (/\ ph ch) (/\ ps ch))
edit