bibif Show Code edit
## Transfer negation by equivalence
thm (bibif () () (-> (-. ps) (<-> (<-> ph ps) (-. ph))) ph ps bi1 con3d com12 ph ps pm5.21 expcom impbid)
(-> (-. ps) (<-> (<-> ph ps) (-. ph)))
edit