bicomd Show Code edit
# Commute two sides of a biconditional in a deduction.
## Commutative Biconditional
thm (bicomd () (bicomd.1 (-> ph (<-> ps ch))) (-> ph (<-> ch ps)) bicomd.1 ps ch bicom sylib)
(-> ph (<-> ch ps))
edit