anidms Show Code edit
## Conjunction is Idempotent
##
## (-> (/\ ph [ ph ) ps)
## (-> [ ph ps)
##
thm (anidms () (anidms.1 (-> (/\ ph ph) ps)) (-> ph ps) anidms.1 ex pm2.43i)
(-> ph ps)
edit