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