anidmdbi Show Code edit
## Conjunction is Idempotent
thm (anidmdbi () () (<-> (-> ph (/\ ps ps)) (-> ph ps)) ps anidm ph imbi2i)
(<-> (-> ph (/\ ps ps)) (-> ph ps))
edit