bibi12i Show Code edit
# The equivalence of two equivalences.
## Combine Two equivalences
thm (bibi12i () (bibi.a (<-> ph ps) bibi12.2 (<-> ch th)) (<-> (<-> ph ch) (<-> ps th)) bibi12.2 ph bibi2i bibi.a th bibi1i bitri)
(<-> (<-> ph ch) (<-> ps th))
edit