3bitr4d Show Code edit
# Deduction from transitivity of biconditional. Useful for converting
# conditional definitions in a formula.
## Transitive Property
thm (3bitr4d () (3bitr4d.1 (-> ph (<-> ps ch)) 3bitr4d.2 (-> ph (<-> th ps)) 3bitr4d.3 (-> ph (<-> ta ch))) (-> ph (<-> th ta)) 3bitr4d.2 3bitr4d.1 3bitr4d.3 bitr4d bitrd)
(-> ph (<-> th ta))
edit