3bitr3rd Show Code edit
# Deduction from transitivity of biconditional.
## Transitive Property
thm (3bitr3rd () (3bitr3d.1 (-> ph (<-> ps ch)) 3bitr3d.2 (-> ph (<-> ps th)) 3bitr3d.3 (-> ph (<-> ch ta))) (-> ph (<-> ta th)) 3bitr3d.3 3bitr3d.1 3bitr3d.2 bitr3d bitr3d)
(-> ph (<-> ta th))
edit