anbi12i Show Code edit
## Conjoin both sides of two equivalences
##
## (<-> ph ] ] ] [ ps ] ] )
## (<-> [ [ ch ] [ [ th ] )
## (<-> (/\ ph ] [ ch ] ) (/\ [ ps [ th ] ))
##
thm (anbi12i () (anbi12.1 (<-> ph ps) anbi12.2 (<-> ch th)) (<-> (/\ ph ch) (/\ ps th)) anbi12.1 ch anbi1i anbi12.2 ps anbi2i bitri)
(<-> (/\ ph ch) (/\ ps th))
edit