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