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