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