3bitr3g Show Code edit
# More general version of [[3bitr3i]]. Useful for converting
# definitions in a formula.
## Transitive Property
thm (3bitr3g () (3bitr3g.1 (-> ph (<-> ps ch)) 3bitr3g.2 (<-> ps th) 3bitr3g.3 (<-> ch ta)) (-> ph (<-> th ta)) 3bitr3g.1 3bitr3g.2 syl5bbr 3bitr3g.3 syl6bb)
(-> ph (<-> th ta))
edit