3bitr3ri Show Code edit
## Transitive Property
thm (3bitr3ri () (1 (<-> ph ps) 2 (<-> ph ch) 3 (<-> ps th)) (<-> th ch)
1 2 3 3bitr3i bicomi)
(<-> th ch)
edit