bicom Show Code edit
# Commutative law for equivalence. Theorem *4.21 of [bib/WhiteheadRussell]
# p. 117.
## Commutative Biconditional
thm (bicom () () (<-> (<-> ph ps) (<-> ps ph)) (-> ph ps) (-> ps ph) ancom ph ps dfbi2 ps ph dfbi2 3bitr4i)
(<-> (<-> ph ps) (<-> ps ph))
edit