ibib Show Code edit
# Implication in terms of implication and biconditional.
## Implication & Biconditional
## left('Simplify', '↔')
thm (ibib () () (<-> (-> ph ps) (-> ph (<-> ph ps))) ph ps pm3.4 ph ps pm3.26 ps a1d impbid ex ph ps bi1 com12 impbid pm5.74i)
(<-> (-> ph ps) (-> ph (<-> ph ps)))
edit