biantrurd Show Code edit
# A wff is equivalent to its conjunction with truth.
thm (biantrurd () (biantrud.1 (-> ph ps)) (-> ph (<-> ch (/\ ps ch))) biantrud.1 ch biantrud ch ps ancom syl6bb)
(-> ph (<-> ch (/\ ps ch)))
edit