ibibr Show Code edit
# Implication in terms of implication and biconditional.
## Implication & Biconditional
## left('Simplify', '↔')
thm (ibibr () () (<-> (-> ph ps) (-> ph (<-> ps ph))) ph ps ibib ph ps bicom ph imbi2i bitri)
(<-> (-> ph ps) (-> ph (<-> ps ph)))
edit