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