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